概率高阶不动点逻辑

摘要：介绍了PHFL，这是高阶不动点逻辑的概率扩展，也可以看作是PCTL和$mu^p$-calculus等概率时态逻辑的高阶扩展。我们表明PHFL比$mu^p$-calculus更具表达能力，对于有限Markov链的PHFL模型检测问题即使对于PHFL的$mu$-only、order-1片段也是不可判定的。此外，完整的PHFL更具表达能力：我们给出了从Lubarsky的$mu$-arithmetic到PHFL的转换，这意味着PHFL模型检测是$Pi^1\_1$-难和$Sigma^1\_1$-难的。作为正面结果，我们使用一种新颖的类型系统为PHFL模型检测问题表征了一个可判定的片段。

作者：Yo Mitani, Naoki Kobayashi and Takeshi Tsukada

论文ID：2011.14303

分类：Logic in Computer Science

分类简称：cs.LO

提交时间：2023-06-22

PDF 下载： 英文版 中文版pdf翻译中