确定化自动机获取的模态μ-演算的证明系统
摘要：无穷对象上的自动机在模态mu-演算理论中占据重要地位。其中一种应用涉及Niwi''{n}ski & Walukiewicz引入的表格游戏，其中对无穷播放的获胜条件可以由非确定性奇偶流自动机自然地检验。受到Jungteerapanich和Stirling的工作的启发，我们展示了如何利用该自动机的确定化构造直接获得$mu$-演算的证明系统。更具体地说，我们引入了一个用于确定化非确定性奇偶流自动机的二叉树构造。利用这个构造，我们定义了带注释的循环证明系统$mathsf{BT}$，其中公式由二进制字符串元组注释。该系统的完备性和正确性几乎立即从确定化方法的正确性得出。
作者：Maurice Dekker, Johannes Kloibhofer, Johannes Marti, Yde Venema
论文ID：2307.06897
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-17