Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site G-Reactive Systems as Coalgebras.
Filippo Bonchi, Ugo Montanari
abstract:
The semantics of process calculi has traditionally been speciŻed by labelled transition systems (LTSs), but with the development of name calculi it turned out that definitions employing reduction semantics
are sometimes more natural. Reactive Systems a la Leifer and Milner allow to derive from a reduction semantics definition an LTS equipped with a bisimilarity relation which is a congruence. This theory has
been extended to G-Reactive Systems by Sassone and Sobocinki in order to properly handle structural equivalence.
Universal Coalgebra provides a categorical framework where bisimilarity can be characterized as final semantics, i.e., each LTS can be mapped to a minimal realization identifying bisimilar states. Moreover, it is often possible to lift coalgebras to an algebraic setting (yielding bialgebras by Turi and Plotkin or, slightly more generally, structured coalgebras by Corradini, Heckel and Montanari) with the property that bisimilarity is compositional with respect to the lifted structure. The existence of minimal realizations is
of theoretical interest, but it is even more of practical interest whenever LTSs are employed for finite state verification.
In this paper we show that for every G-Reactive System we can build a coalgebra. Furthermore, if bisimilarity is compositional in the Reactive System, then we can lift this coalgebra to a structured coalgebra.
