Tableaux and Algorithms for Propositional Dynamic Logic with Converse
Tableaux and Algorithms for Propositional Dynamic Logic with Converse
复制标题
DOI：
10.1007/3-540-61511-3_117
复制
发表时间：
1996-08
期刊：
影响因子：
--
通讯作者：
Giuseppe De Giacomo;F. Massacci
中科院分区：
文献类型：
--
作者：
Giuseppe De Giacomo;F. Massacci
本文提出了一种基于不同技术的命题动态逻辑的前缀表演算，包括用于模态逻辑的前缀表演算和用于u演算的模型检查器。我们证明了该演算的正确性和完备性，并说明了它的性质。我们还讨论了Tableaux方法(朴素的NEXPTIME)到EXPTIME算法的转换。
This paper presents a prefixed tableaux calculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for mu-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME algorithm.