A Logic of Probability with Decidable Model Checking
A Logic of Probability with Decidable Model Checking
复制标题
DOI：
10.1093/logcom/exl004
复制
发表时间：
2006-08
期刊：
影响因子：
--
通讯作者：
D. Beauquier;A. Rabinovich;A. Slissenko
中科院分区：
文献类型：
--
作者：
D. Beauquier;A. Rabinovich;A. Slissenko
介绍了一种与Halpern等人的概率逻辑相近的概率谓词逻辑。我们的主要结果涉及以下模型检验问题：确定给定公式是否适用于由给定有限概率过程定义的结构。我们证明了对于二阶一元概率逻辑中相当大的公式子类，这个模型检验问题是可判定的。我们还讨论了可满足性的可判断性，并将我们的概率逻辑与概率时序逻辑PCTL*进行了比较。
A predicate logic of probability, close to the logics of probability of Halpern et al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given finite probabilistic process. We show that this model-checking problem is decidable for a rather large subclass of formulas of a second-order monadic logic of probability. We discuss also the decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCTL*.