In this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification Gamma. More precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of Gamma-algebras. The systems we consider are specified by using arbitrary SOS rules, which in general do not guarantee that bisimilarity is a congruence. We first show that the structured coalgebra representation works only for systems where transitions out of complex states can be derived from transitions out of corresponding component states. This decomposition property of transitions indeed ensures that bisimilarity is a congruence. For a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i.e., transitions that spontaneously embed a state into a bigger context or vice versa. The notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, i.e., with the coarsest bisimulation which is a congruence. This is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction. (C) 2002 Elsevier Science B.V. All rights reserved.
Compositional SOS and beyond: a coalgebraic view of open systems
CORRADINI, ANDREA;MONTANARI, UGO GIOVANNI ERASMO
2002-01-01
Abstract
In this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification Gamma. More precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of Gamma-algebras. The systems we consider are specified by using arbitrary SOS rules, which in general do not guarantee that bisimilarity is a congruence. We first show that the structured coalgebra representation works only for systems where transitions out of complex states can be derived from transitions out of corresponding component states. This decomposition property of transitions indeed ensures that bisimilarity is a congruence. For a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i.e., transitions that spontaneously embed a state into a bigger context or vice versa. The notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, i.e., with the coarsest bisimulation which is a congruence. This is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction. (C) 2002 Elsevier Science B.V. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
