Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Layered automata: A canonical model for automata over infinite words

Antonio Casares, Christof Löding, Igor Walukiewicz

TL;DR

The work addresses the absence of a canonical minimal representation for $\\omega$-regular languages by introducing layered automata, a structured extension of alternating parity automata. Under a consistency condition, layered automata become history deterministic and 0-1 probabilistic, enabling polynomial-time canonicity, minimisation, and efficient decision procedures. The authors show that every $\\omega$-regular language has a unique minimal consistent layered automaton and provide a congruence-based characterization of the minimal form, with a polynomial-time construction from any consistent layered automaton. They also relate layered automata to established models (deterministic/alternating automata, COCOA, Zielonka trees, signature automata) and discuss implications for verification and synthesis, including potential size advantages over DPAs. Overall, the framework yields a robust, computable, and compositional canonical representation for all $\\omega$-regular languages, with practical relevance to model checking and synthesis tasks that require canonical, compact representations.

Abstract

We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that for layered automata both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.

Layered automata: A canonical model for automata over infinite words

TL;DR

The work addresses the absence of a canonical minimal representation for -regular languages by introducing layered automata, a structured extension of alternating parity automata. Under a consistency condition, layered automata become history deterministic and 0-1 probabilistic, enabling polynomial-time canonicity, minimisation, and efficient decision procedures. The authors show that every -regular language has a unique minimal consistent layered automaton and provide a congruence-based characterization of the minimal form, with a polynomial-time construction from any consistent layered automaton. They also relate layered automata to established models (deterministic/alternating automata, COCOA, Zielonka trees, signature automata) and discuss implications for verification and synthesis, including potential size advantages over DPAs. Overall, the framework yields a robust, computable, and compositional canonical representation for all -regular languages, with practical relevance to model checking and synthesis tasks that require canonical, compact representations.

Abstract

We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that for layered automata both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.
Paper Structure (37 sections, 21 theorems, 13 equations, 5 figures)

This paper contains 37 sections, 21 theorems, 13 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Applicability.
  3. Canonicity, morphisms, and congruences.
  4. Minimisation in PTIME.
  5. Relation to other models.
  6. Preliminaries
  7. Transition systems.
  8. Deterministic parity automata.
  9. Alternating parity automata.
  10. Semantic determinism.
  11. Resolvers and history determinism.
  12. Layered automata
  13. Syntactic definition of layered automata
  14. The forest of a layered automaton.
  15. Semantics via alternating parity automata
  16. ...and 22 more sections

Key Result

Theorem 1

Every "$\omega$-regular language" $L$ can be recognised by a "consistent" "layered automaton" $\mathcal{A}_L$ such that every equivalent "consistent" "layered automaton" contains a "subautomaton" admitting a surjective "morphism@@lay" to $\mathcal{A}_L$. Moreover, $\mathcal{A}_L$ can be computed in

Figures (5)

  • Figure 1: Two "layered automata", represented as trees.
  • Figure 2: Alternating parity automaton for the "layered automaton" on the left of Figure \ref{['fig:layered-example-trees']}.
  • Figure 3: Alternating parity automaton for the "layered automaton" on the right of Figure \ref{['fig:layered-example-trees']}.
  • Figure 4: The layered automaton for $k=4$ in Example \ref{['ex:COCOA-to-layered-exponential']}. In each SCC on each layer, all edges going to the same state have the same label. For readability, we have omitted the labels for the edges from right to left on layers 2 and 3.
  • Figure 5: The layered automaton for $k=4$ in Example \ref{['ex:COCOA-exponential-product']}.

Theorems & Definitions (34)

  • Theorem 1
  • Remark 2
  • Example 3
  • Remark 4
  • Definition 5
  • Lemma 6
  • Remark 7
  • Example 8
  • Example 9
  • Proposition 10
  • ...and 24 more