@article {BMS13,
	title = {Sound and complete axiomatizations of coalgebraic language equivalence},
	journal = {ACM Transactions on Computational Logic (TOCL)},
	volume = {14},
	number = {1},
	year = {2013},
	pages = {1-51},
	publisher = {ACM},
	abstract = {<p>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 determinized 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{\textquoteright}s sound and complete calculus for language equivalence.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/xana/files/1104.2803v4.pdf},
	author = {Marcello Bonsangue and Stefan Milius and Alexandra Silva}
}