A Recursive Probabilistic Temporal Logic

PABLO F. CASTRO; CECILIA KILMURRAY; NIR PITERMAN

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlin; Año: 2015 vol. 9407 p. 336 - 348

0302-9743

In this paper we introduce recursive probabilistic computation-tree logic as a restriction of μPCTLμPCTL. We introduce the logic in detail and show its usefulness for verifying systems. We illustrate this by means of some examples. Roughly speaking, we include recursive operators within pctl, which enable one to identify repeating patterns of probability. This new feature seems in particular useful for expressing properties regarding stability of system executions; such properties are usual, for instance, in those scenarios where one is interested to verify whether the system under verification stays in, or revisits, a subset of safe states. Also, the logic makes it possible to reason about set of executions with zero measure; something no possible in related logics.