论文标题
概率的高阶FixPoint逻辑
A Probabilistic Higher-order Fixpoint Logic
论文作者
论文摘要
我们介绍了PHFL，这是高阶FixPoint逻辑的概率扩展，也可以被视为概率时间逻辑（例如PCTL和$μ^p $ -calculus）的高阶扩展。我们表明，PHFL比$μ^p $ -calculus更具表现力，并且即使对于仅$μ$的PHFL订单-1片段，有限马尔可夫链的PHFL模型检查问题也无法确定。此外，完整的PHFL具有更大的表现力：我们将Lubarsky的$μ$ -URITHMETIC转换为PHFL，这意味着PHFL模型检查为$π^1_1 $ -HARD和$σ^1_1 $ -HARD。作为积极的结果，我们表征了使用新型类型系统的PHFL模型检查问题的可决定片段。
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $μ^p$-calculus. We show that PHFL is strictly more expressive than the $μ^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $μ$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $μ$-arithmetic to PHFL, which implies that PHFL model checking is $Π^1_1$-hard and $Σ^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.
