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

TL;DR

This paper extends a subclass of mu-calculus with freeze quantifiers to infinite words, demonstrating its expressive equivalence to Buchi Register Automata for infinite data words.

Contribution

It redefines the disjunctive mu-downarrow calculus for infinite words and proves its expressive power matches Buchi Register Automata.

Findings

Equivalent expressive power to Buchi Register Automata for infinite words

Redefinition of mu-calculus for infinite data words

Theoretical proof of expressiveness equivalence

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.