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.