Bonsangue M, Milius S, Silva A (2013)
Publication Type: Journal article
Publication year: 2013
Publisher: Association for Computing Machinery (ACM)
Book Volume: 14
Pages Range: 1-52
Journal Issue: 1:7
Coalgebras provide a uniform framework for studying dynamical systems, including several types of automata. In this article, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalized powerset construction that determinizes coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor FT, where T is a monad describing the branching of the systems (e.g., non-determinism, weights, probability, etc.), has as a quotient the rational fixpoint of the deter-minized type functor F, a lifting of F to the category of T-algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain nondeterministic automata in which we recover Rabinovich's sound and complete calculus for language equivalence. © 2013 ACM 1529-3785/2013/02-ART7 $15.00.
APA:
Bonsangue, M., Milius, S., & Silva, A. (2013). Sound and Complete Axiomatizations of Coalgebraic Language Equivalence. ACM Transactions on Computational Logic, 14(1:7), 1-52. https://doi.org/10.1145/2422085.2422092
MLA:
Bonsangue, Marcello, Stefan Milius, and Alexandra Silva. "Sound and Complete Axiomatizations of Coalgebraic Language Equivalence." ACM Transactions on Computational Logic 14.1:7 (2013): 1-52.
BibTeX: Download