Tableau systems for the modal μ-calculus
Tableau systems for the modal μ-calculus
复制标题
用于模态 μ 演算的 Tableau 系统
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Natthapong Jungteerapanich
中科院分区：
文献类型：
--
作者：
Natthapong Jungteerapanich
本论文的主要内容涉及一种求解模态μ微积分可满足性问题的表格方法。给出了一个完善的、完整的模态μ演算表系统。由于这种表格系统中的每个表格都是有限的并且受公式的长度限制，因此该表格系统可以用作确定公式的可满足性的决策过程。得到了小模型性质的另一种证明：每个可满足的公式都有一个大小为公式长度的单指数的模型。与文献中的已知证明相反，这里给出的结果不依赖于自动机理论。给出了画面系统的两种简化。一类是连接公式类。由此产生的表格系统已被用来证明 Kozen 公理化关于模态 μ 微积分的合取片段的完整性。另一个是类 Πμ2 中的公式。除了tableau方法之外，本文还探索了一些模型手术技术，旨在将这些技术用于直接证明小模型定理。迄今为止获得的技术已用于显示 Πμ2 公式和线性模型公式的小模型属性。
The main content of this thesis concerns a tableau method for solving the satisfiability problem for the modal μ-calculus. A sound and complete tableau system for the modal μ-calculus is given. Since every tableau in such tableau system is finite and bounded by the length of the formula, the tableau system may be used as a decision procedure for determining the satisfiability of the formula. An alternative proof of the small model property is obtained: every satisfiable formula has a model of size singleexponential in the length of the formula. Contrary to known proofs in literature, the results presented here do not rely on automata theory. Two simplifications of the tableau system are given. One is for the class of aconjunctive formulae. The resulting tableau system has been used to prove the completeness of Kozen’s axiomatisation with respect to the aconjunctive fragment of the modal μcalculus. Another is for the formulae in the class Πμ2 . In addition to the tableau method, the thesis explores some model-surgery techniques with the aim that such techniques may be used to directly prove the small model theorem. The techniques obtained so far have been used to show the small model property for Πμ2 -formulae and for formulae with linear models.