Tractable Probabilistic μ-Calculus that Expresses Probabilistic Temporal Logics

We revisit a recently introduced probabilistic μ-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 μ-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP intersection 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 μ-calculus.