Coalgebraic Trace Semantics for Buechi and Parity Automata

TL;DR

This paper extends coalgebraic trace semantics to Buechi and parity automata, providing a uniform, diagram-based characterization of accepted languages for infinite words and trees, applicable to nondeterministic and probabilistic systems.

Contribution

It introduces a coalgebraic framework for Buechi and parity automata using commuting diagrams, unifying the semantics across different automata types and acceptance conditions.

Findings

Characterizes Buechi automata languages via two commuting diagrams.

Applies the framework uniformly to nondeterministic and probabilistic automata.

Extends the approach to parity acceptance conditions for infinite structures.

Abstract

Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.