2011/04/30 by Marcello M. Bonsangue, Stefan Milius, Alexandra Silva · 1 citation
Computer Science · Mathematics · #cs.LO #math.CT
paper · pdf · doi:10.1145/2422085.2422092
published as ACM Transactions on Computational Logic (TOCL) 14:1, Article No. 7, ACM, Feb. 2013 · Corrected version of published journal article
arxiv created 2017/03/17 · arxiv updated 2017/03/20
Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, 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 generalised powerset construction that determinises 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 "determinised" 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 non-deterministic automata, where we recover Rabinovich's sound and complete calculus for language equivalence.