A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
<|reference_start|>A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata: Register automaton (RA) is an extension of finite automaton for dealing with data values in an infinite domain. In the previous work, we proposed disjunctive mu$^\downarrow$-calculus, which is a subclass of modal mu-calculus with the freeze quantifier, and showed that it has the same expressive power as RA. However, disjunctive mu$^\downarrow$-calculus is defined as a logic on finite words, whereas temporal specifications in model checking are usually given in terms of infinite words. In this paper, we re-define the syntax and semantics of disjunctive mu$^\downarrow$-calculus to be suitable for infinite words and prove that the obtained temporal logic has the same expressive power as Buchi RA.<|reference_end|>
@article{takata2024a,
    title={A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi
  Register Automata},
    author={Yoshiaki Takata, Akira Onishi, Ryoma Senda, Hiroyuki Seki},
    journal={arXiv preprint arXiv:2406.11351},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.11351},
    primaryClass={cs.FL cs.LO}
}