Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rerailing Automata

Rüdiger Ehlers

TL;DR

Rerailing automata provide a polynomial-time minimizable representation for $ω$-regular languages that generalizes both deterministic parity automata and minimized history-deterministic co-Büchi automata with transition-based acceptance. The key idea is to define acceptance via the maximum dominating color across all runs and to enforce a rerailing property that guarantees a prefix can be extended to a uniform, even dominating color behavior once a rerailing point is reached; this enables a structured, residual-language-based minimization. The paper develops floating co-Büchi automata as an essential intermediate model, proves a central nesting theorem linking rerailing SCCs to COCOA components, and presents a recursive construction that yields minimal rerailing automata from chains of COCOA with polynomial-time complexity. These results imply that rerailing automata can replace deterministic parity automata in realizability checks and may improve synthesis and verification workflows, while preserving a close relationship to established ω-regular representations. The work opens avenues for probabilistic extensions and further size comparisons with DPAs, and lays groundwork for leveraging the central nesting structure in practical algorithmic pipelines.

Abstract

In this paper, we introduce rerailing automata for $ω$-regular languages. They generalize both deterministic parity (DPW) and minimized history-deterministic co-Büchi automata (with transition based acceptance, HdTbcBW) while combining their favorable properties. In particular, rerailing automata can represent arbitrary $ω$-regular languages while allowing for polynomial-time minimization, just as HdTbcBW do. Since DPW are a special case of rerailing automata, a minimized rerailing automaton is never larger than the smallest deterministic parity automaton for the same language. We also show that rerailing automata can be used as a replacement for deterministic parity automata for the realizability check of open systems. The price to be paid to obtain the useful properties of rerailing automata is that the acceptance condition in such automata refers to the dominating colors along all runs for a given word, where just as in parity automata, the dominating color along a run is the lowest one occurring infinitely often along it. A rerailing automaton accepts those words for which the greatest of the dominating colors along the runs is even. Additionally, rerailing automata guarantee that every prefix of a run for a word can be extended to eventually reach a point from which all runs for the word extending the prefix have the same dominating color, and it is even if and only if the word is in the language of the automaton. We show that these properties together allow characterizing the role of each state in such an automaton in a way that relates it to state combinations in a sequence of co-Büchi automata for the represented language. This characterization forms the basis of the polynomial-time minimization approach in this paper.

Rerailing Automata

TL;DR

Rerailing automata provide a polynomial-time minimizable representation for -regular languages that generalizes both deterministic parity automata and minimized history-deterministic co-Büchi automata with transition-based acceptance. The key idea is to define acceptance via the maximum dominating color across all runs and to enforce a rerailing property that guarantees a prefix can be extended to a uniform, even dominating color behavior once a rerailing point is reached; this enables a structured, residual-language-based minimization. The paper develops floating co-Büchi automata as an essential intermediate model, proves a central nesting theorem linking rerailing SCCs to COCOA components, and presents a recursive construction that yields minimal rerailing automata from chains of COCOA with polynomial-time complexity. These results imply that rerailing automata can replace deterministic parity automata in realizability checks and may improve synthesis and verification workflows, while preserving a close relationship to established ω-regular representations. The work opens avenues for probabilistic extensions and further size comparisons with DPAs, and lays groundwork for leveraging the central nesting structure in practical algorithmic pipelines.

Abstract

In this paper, we introduce rerailing automata for -regular languages. They generalize both deterministic parity (DPW) and minimized history-deterministic co-Büchi automata (with transition based acceptance, HdTbcBW) while combining their favorable properties. In particular, rerailing automata can represent arbitrary -regular languages while allowing for polynomial-time minimization, just as HdTbcBW do. Since DPW are a special case of rerailing automata, a minimized rerailing automaton is never larger than the smallest deterministic parity automaton for the same language. We also show that rerailing automata can be used as a replacement for deterministic parity automata for the realizability check of open systems. The price to be paid to obtain the useful properties of rerailing automata is that the acceptance condition in such automata refers to the dominating colors along all runs for a given word, where just as in parity automata, the dominating color along a run is the lowest one occurring infinitely often along it. A rerailing automaton accepts those words for which the greatest of the dominating colors along the runs is even. Additionally, rerailing automata guarantee that every prefix of a run for a word can be extended to eventually reach a point from which all runs for the word extending the prefix have the same dominating color, and it is even if and only if the word is in the language of the automaton. We show that these properties together allow characterizing the role of each state in such an automaton in a way that relates it to state combinations in a sequence of co-Büchi automata for the represented language. This characterization forms the basis of the polynomial-time minimization approach in this paper.

Paper Structure

This paper contains 22 sections, 20 theorems, 7 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Introducing rerailing automata
  4. Analyzing the properties of minimal history-deterministic co-Büchi automata
  5. Defining rerailing automata
  6. Some properties of Rerailing Automata
  7. Decomposing the Structure of Rerailing automata
  8. Preparation: Floating co-Büchi automata
  9. How SCCs need to be nested in rerailing automata
  10. Building minimal rerailing automaton
  11. Preparation: Computing the residual language tracking automaton for a given chain of co-Büchi automata
  12. Building the Rerailing automaton
  13. Application: Realizability Checking for Reactive Systems
  14. Related work
  15. Conclusion & Outlook
  16. ...and 7 more sections

Key Result

Proposition 1

Let $\mathcal{A}$ be a deterministic parity automaton. We have that $\mathcal{A}$ is also a rerailing automaton and $\mathcal{L}_\mathit{rerail}(\mathcal{A}) = \mathcal{L}_\mathit{parity}(\mathcal{A})$.

Figures (6)

  • Figure 1: An example minimized HdTbcBW over the alphabet $\Sigma = \{a,b,c\}$
  • Figure 2: An example chain of minimized floating co-Büchi automata for a uniform residual lanaguage over $\Sigma= \{a,b,c,d\}$
  • Figure 3: A minimal rerailing automaton over the alphabet $\Sigma = \{a,b,c\}$. Dashed lines represent cases in which transitions to all states (including the state from which the transition starts) exist.
  • Figure 4: The automata $\mathcal{A}^1$ and $\mathcal{A}^2$ in a chain of co-Büchi automata $\mathcal{A}^1,\mathcal{A}^2$ for which the number of residual languages in the indivdiual co-Büchi automata is larger than the number of residual languages of the overall language represented by the chain.
  • Figure 5: Algorithm for computing a residual language tracking automaton $R^L$ from a chain of history-deterministic co-Büchi automata $\mathcal{A}^1, \ldots, \mathcal{A}^n$
  • ...and 1 more figures

Theorems & Definitions (49)

  • Definition 1
  • Proposition 1
  • proof
  • Proposition 2
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Definition 2
  • Lemma 3
  • ...and 39 more