Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics
Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics
复制标题
DOI：
10.4230/lipics.stacs.2015.211
复制
发表时间：
2015-02
期刊：
影响因子：
--
通讯作者：
Pablo F. Castro;C. Kilmurray;Nir Piterman
中科院分区：
文献类型：
--
作者：
Pablo F. Castro;C. Kilmurray;Nir Piterman
我们重新审视了最近引入的概率μ演算，并研究了它的一个表达片段，通过将概率量化作为演算的原子运算，我们建立了演算与义务博弈之间的联系.我们考虑的演算足够强大，可以对诸如pctl和pctl^* 之类的著名逻辑进行编码。它的博弈语义与经典μ演算的博弈语义非常相似（使用平价义务博弈而不是平价博弈）。这导致NP\cap co-NP的有限模型检验过程的最佳复杂度。此外，我们研究了这个演算的一个（相对）表现良好的片段：具有不动点的pctl的扩展。这个pctl扩展版本的一个重要特性是它的模型检查只是指数w.r.t.。不动点的交替深度，这是Kozen μ演算的主要特征之一。
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 NP\cap 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.