A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata

Yoshiaki Takata, Akira Onishi, Ryoma Senda +1

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 }$-calcul…