Coalgebraic models for reactive systems

Abstract

Reactive Systems àla Leifer and Milner allow to derive from a reaction semantics definition an LTS equipped with a bisimilarity relation which is a congruence. This theory has been extended by the authors (together with Barbara König) in order to handle saturated bisimilarity, a coarser equivalence that is more adequate for some interesting formalisms, such as logic programming and open pi-calculus. In this paper we recast the theory of Reactive Systems inside Universal Coalgebra. This construction is particularly useful for saturated bisimilarity, which can be seen as final semantics of Normalized Coalgebras. These are structured coalgebras (not bialgebras) where the sets of transitions are minimized rather than maximized as in saturated LTS, still yielding the same semantics. We give evidence the effectiveness of our approach minimizing an Open Petri net in a category of Normalized Coalgebras. © Springer-Verlag Berlin Heidelberg 2007.