Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata
Lecture Notes in Computer Science(2023)
摘要
Automata operating on infinite objects feature prominently in the theory of the modal $\mu$-calculus. One such application concerns the tableau games introduced by Niwi\'{n}ski & Walukiewicz, of which the winning condition for infinite plays can be naturally checked by a nondeterministic parity stream automaton. Inspired by work of Jungteerapanich and Stirling we show how determinization constructions of this automaton may be used to directly obtain proof systems for the $\mu$-calculus. More concretely, we introduce a binary tree construction for determinizing nondeterministic parity stream automata. Using this construction we define the annotated cyclic proof system $\mathsf{BT}$, where formulas are annotated by tuples of binary strings. Soundness and Completeness of this system follow almost immediately from the correctness of the determinization method.
更多查看译文
关键词
determinizing
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要