论文标题
无限状态系统的可扩展证明系统
Extensible Proof Systems for Infinite-State Systems
论文作者
论文摘要
本文重新审视了证明无限状态标记过渡系统状态的证明系统的完整性和完整性，使模态MU-Calculus中的公式满足公式。我们的结果依赖于晶格理论的新成果，从而在完整的晶格上赋予了单调功能的最大和最小固定点的建设性特征。我们展示了如何使用这些结果来重建由于布拉德菲尔德和斯特林而导致此问题的声音和完整的图表方法。我们还展示了我们的晶格理论基础的灵活性如何简化有关替代类别系统基于图表的证明策略的推理。特别是，我们以定时模态扩展了模态MU-Calculus，并证明所得的Tableaux方法是合理的，并且对于定时过渡系统是完整的。
This paper revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calculus. Our results rely on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used to reconstruct the sound and complete tableau method for this problem due to Bradfield and Stirling. We also show how the flexibility of our lattice-theoretic basis simplifies reasoning about tableau-based proof strategies for alternative classes of systems. In particular, we extend the modal mu-calculus with timed modalities, and prove that the resulting tableaux method is sound and complete for timed transition systems.
