paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Finite Satisfiability Problem for PCTL is Undecidable

PCTL 的有限可满足性问题是不可判定的
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10 · 该论文研究 PCTL 有限可满足性与有限状态 Markov 链有效性的不可判定性，属于纯逻辑/概率模型检验理论，与用户关注的 LLM+静态分析、浮点程序分析、贝叶斯程序分析及 Agentic 程序分析均无直接关系。虽涉及形式化验证的逻辑基础，但既无 LLM/Agent 交叉，也无程序分析或工业落地内容。引用 2 inbox
Miroslav Chodil, Antonín Kučera
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：证明 PCTL 的有限可满足性不可判定，甚至受限公式类和有限状态 Markov 链有效性也不可半判定。

论文研究 PCTL 公式是否存在有限模型的问题，即给定 PCTL 公式，判定其是否可被某个有限状态 Markov 链满足。作者证明该有限可满足性问题是不可判定的。该不可判定性结果即使对一类形式为 [EQUATION] 的受限公式仍然成立，其中子公式 φ1、φ2 的有效性仅依赖于至多两步转移内可达的状态。作为推论，判定一个 PCTL 公式是否在所有有限状态 Markov 链中有效也不是可半判定的。该工作明确了 PCTL 在有限模型语义下的可判定性边界，说明其有限可满足性与有限状态全局有效性均超出可判定范围。

问题
给定 PCTL 公式，判定它是否存在有限状态 Markov 链模型，即 PCTL 的有限可满足性问题。
方法
通过不可判定性证明，将结果加强到一类受限 PCTL 公式，其子公式有效性仅依赖至多两步可达状态。
评估
以可判定性与复杂度分析为评估方式，证明有限可满足性不可判定，并推出有限状态 Markov 链上的全局有效性不可半判定。
原文摘要（Abstract）

We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form [EQUATION] where the validity of ϕ1, ϕ2 depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.

链接与引用

DOI 原文 · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{Chodil024,
  title = {The Finite Satisfiability Problem for PCTL is Undecidable},
  author = {Miroslav Chodil and Antonín Kučera},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662145}
}