Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Yoshiaki Takata, Akira Onishi, Ryoma Senda, Hiroyuki Seki

TL;DR

The paper addresses the problem of specifying and verifying properties of systems that manipulate data values over infinite executions. It defines ${\mathrm{\mu^\downarrow}}_{\mathrm{d}\omega}$-calculus, a temporal logic with a freeze quantifier suitable for infinite data words, and proves it has the same expressive power as Büchi register automata by providing constructive translations in both directions. The authors establish formal semantics using environments and 5-tuples to capture least and greatest fixed points, and validate the correctness of transformations with the Coq proof assistant. This work enables automata-theoretic verification methods for data-rich temporal specifications and lays groundwork for RA-based model checking and verification workflows, with future directions toward formal verification methods grounded in BRA.

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.

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

TL;DR

The paper addresses the problem of specifying and verifying properties of systems that manipulate data values over infinite executions. It defines -calculus, a temporal logic with a freeze quantifier suitable for infinite data words, and proves it has the same expressive power as Büchi register automata by providing constructive translations in both directions. The authors establish formal semantics using environments and 5-tuples to capture least and greatest fixed points, and validate the correctness of transformations with the Coq proof assistant. This work enables automata-theoretic verification methods for data-rich temporal specifications and lays groundwork for RA-based model checking and verification workflows, with future directions toward formal verification methods grounded in BRA.

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-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-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-calculus to be suitable for infinite words and prove that the obtained temporal logic has the same expressive power as Buchi RA.
Paper Structure (7 sections, 5 theorems, 14 equations, 1 figure)

This paper contains 7 sections, 5 theorems, 14 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Disjunctive $\mu$-calculus with the freeze quantifier (${\mu^\downarrow}_{\!\mathrm{d}\omega}$-calculus)
  4. Büchi register automata
  5. Transformation from ${\mu^\downarrow}_{\!\mathrm{d}\omega}$-calculus into Büchi RA
  6. Transformation from Büchi RA into ${\mu^\downarrow}_{\!\mathrm{d}\omega}$-calculus
  7. Conclusion

Key Result

Lemma 1

Let $\sigma$ be a system of equations in ${\mu^\downarrow}_{\!\mathrm{d}\omega}$-calculus. We can translate $\sigma$ into an equivalent system $\sigma'$ that consists of equations of the form $V=V'\lor V"$, $V=\mathord{\downarrow}_R\mathord{\mathsf{X}} V'\land\phi$, or $V=\mathtt{tt}$ where $V,V',V"

Figures (1)

  • Figure 1: Büchi RA equivalent to $\{\,V_{\mathtt{tt}}=\mathtt{tt}$, $V_1 = \mathord{\uparrow}_1$, $V_2 = V_1 \lor(\mathord{\mathsf{X}} V_2\land (\neg\mathord{\uparrow}_1\land p_1))$, $V_3 = \mathord{\downarrow}_1\mathord{\mathsf{X}} V_2 \,\}$ when $\mathit{Var}_{\omega}=\{V_{\mathtt{tt}}\}$.

Theorems & Definitions (19)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Example 1
  • ...and 9 more