Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors

TL;DR

This paper develops a categorical framework for modeling automaton acceptance conditions, specifically Buechi and parity, using alternating fixed points of functors, advancing the theoretical understanding of system behaviors.

Contribution

It introduces a novel categorical construction of alternating fixed points of functors, enabling abstract modeling of Buechi and parity acceptance conditions in automata theory.

Findings

Categorical modeling of acceptance conditions using alternating fixed points

Abstracts automaton states to system behaviors

Provides a new theoretical foundation for automata with Buechi and parity conditions

Abstract

Categorical studies of recursive data structures and their associated reasoning principles have mostly focused on two extremes: initial algebras and induction, and final coalgebras and coinduction. In this paper we study their in-betweens. We formalize notions of alternating fixed points of functors using constructions that are similar to that of free monads. We find their use in categorical modeling of accepting run trees under the Buechi and parity acceptance condition. This modeling abstracts away from states of an automaton; it can thus be thought of as the "behaviors" of systems with the Buechi or parity conditions, in a way that follows the tradition of coalgebraic modeling of system behaviors.