Layered automata: A canonical model for automata over infinite words

TL;DR

This paper introduces layered automata, a new subclass of automata over infinite words that generalizes deterministic automata, providing a canonical minimal form and efficient algorithms for key decision problems.

Contribution

The paper defines layered automata, proves their canonical minimal form exists and can be computed efficiently, and establishes polynomial-time algorithms for consistency and inclusion testing.

Findings

Every omega-regular language has a unique minimal consistent layered automaton.

Minimal layered automata can be computed in polynomial time from any layered or deterministic automaton.

Consistency checking and inclusion testing for layered automata are polynomial-time procedures.

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.