This paper relates labeled transition systems and coalgebras with the motivation of comparing and combining their complementary contributions to the theory of concurrent systems. The well-known mismatch between these two notions for what concerns the morphisms is resolved by extending the coalgebraic framework by lax cohomomorphisms. Enriching both labeled transition systems and coalgebras with algebraic structure for an algebraic specification, the correspondence is lost again. This leads to the introduction of lax coalgebras, where the coalgebra structure is given by a lax homomorphism. The resulting category of lax coalgebras and lax cohomomorphisms for a suitable endofunctor is shown to be isomorphic to the category of structured transition systems, where both states and transitions form algebras. The framework is also presented on a more abstract categorical level using monads and comonads, extending the bialgebraic approach recently introduced by Turi and Plotkin.
Structured Transition Systems as Lax Coalgebras
CORRADINI, ANDREA;
1998-01-01
Abstract
This paper relates labeled transition systems and coalgebras with the motivation of comparing and combining their complementary contributions to the theory of concurrent systems. The well-known mismatch between these two notions for what concerns the morphisms is resolved by extending the coalgebraic framework by lax cohomomorphisms. Enriching both labeled transition systems and coalgebras with algebraic structure for an algebraic specification, the correspondence is lost again. This leads to the introduction of lax coalgebras, where the coalgebra structure is given by a lax homomorphism. The resulting category of lax coalgebras and lax cohomomorphisms for a suitable endofunctor is shown to be isomorphic to the category of structured transition systems, where both states and transitions form algebras. The framework is also presented on a more abstract categorical level using monads and comonads, extending the bialgebraic approach recently introduced by Turi and Plotkin.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.