Coalgebraic Trace Semantics for Buechi and Parity Automata
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.
Keywords
Cite
@article{arxiv.1606.09399,
title = {Coalgebraic Trace Semantics for Buechi and Parity Automata},
author = {Natsuki Urabe and Shunsuke Shimizu and Ichiro Hasuo},
journal= {arXiv preprint arXiv:1606.09399},
year = {2016}
}
Comments
A preprint version of the paper to appear in CONCUR 2016; with appendices