Sound and Complete Axiomatizations of Coalgebraic Language Equivalence

Bonsangue M, Milius S, Silva A (2013)


Publication Type: Journal article

Publication year: 2013

Journal

Publisher: Association for Computing Machinery (ACM)

Book Volume: 14

Pages Range: 1-52

Journal Issue: 1:7

DOI: 10.1145/2422085.2422092

Abstract

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.

Authors with CRIS profile

Involved external institutions

How to cite

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://dx.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