2016/06/30 by Natsuki Urabe, Urabe, Natsuki, Shunsuke Shimizu +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1606.09399
openalex publication_date 2016/06/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.