1. A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
- Author
-
Takata, Yoshiaki, Onishi, Akira, Senda, Ryoma, and Seki, Hiroyuki
- Subjects
Computer Science - Formal Languages and Automata Theory ,Computer Science - Logic in Computer Science - Abstract
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., Comment: 6 pages, 1 figure, this is a longer version of a short paper submitted to IEICE Transactions on Information and Systems
- Published
- 2024