Proof Systems for the Modal -Calculus Obtained by Determinizing Automata
Lecture Notes in Computer Science(2023)
Abstract
Automata operating on infinite objects feature prominently in the theory of the modal mu-calculus. One such application concerns the tableau games introduced by Niwinski & Walukiewicz, of which the winning condition for infinite plays can be naturally checked by a non-deterministic 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 non-deterministic parity stream automata. Using this construction we define the annotated cyclic proof system 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.
MoreTranslated text
Key words
modal mu-calculus,derivation system,determinisation of Buchi and parity automata,non-wellfounded and cyclic proofs
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined