Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics

PABLO F. CASTRO; CECILIA KILMURRAY; NIR PITERMAN

Leibniz International Proceedings in Informatics

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Año: 2015 vol. 30 p. 211 - 223

We revisit a recently introduced probabilistic mu-calculus and study an expressive fragment of it. By using the probabilistic quantification as an atomic operation of the calculus we establish a connection between the calculus and obligation games. The calculus we consider is strong enough to encode well-known logics such as pctl and pctl^*. Its game semantics is very similar to the game semantics of the classical mu-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NPcap co-NP for its finite model checking procedure. Furthermore, we investigate a (relatively) well-behaved fragment of this calculus: an extension of pctl with fixed points. An important feature of this extended version of pctl is that its model checking is only exponential w.r.t. the alternation depth of fixed points, one of the main characteristics of Kozen´s mu-calculus.