Labeled state-to-function transition systems, FuTSs for short, capture transition schemes incorporat- ing multiplicities from states to functions of finite support over general semirings. As such FuTSs constitute a convenient modeling instrument to deal with process languages and their stochastic ex- tensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity co- incides with behavioural equivalence of the associated functor. Moreover, it is shown that for FuTSs involving a specific type of semiring only, weak pullbacks are preserved. As a consequence, for these FuTSs, behavioural equivalence coincides with coalgebraic bisimilarity. As generic examples, the equivalences underlying the stochastic process algebras PEPA and IML are related to the bisimilar- ity of specific FuTSs. By the correspondence result coalgebraic justification of the equivalences of these calculi is obtained. Further illustrations of FuTS semantics are discussed for deterministically (discrete) timed process algebras and Markov Automata.
TR 09: Coalgebraic bisimulation of FuTS
Latella D;Massink M;
2013
Abstract
Labeled state-to-function transition systems, FuTSs for short, capture transition schemes incorporat- ing multiplicities from states to functions of finite support over general semirings. As such FuTSs constitute a convenient modeling instrument to deal with process languages and their stochastic ex- tensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity co- incides with behavioural equivalence of the associated functor. Moreover, it is shown that for FuTSs involving a specific type of semiring only, weak pullbacks are preserved. As a consequence, for these FuTSs, behavioural equivalence coincides with coalgebraic bisimilarity. As generic examples, the equivalences underlying the stochastic process algebras PEPA and IML are related to the bisimilar- ity of specific FuTSs. By the correspondence result coalgebraic justification of the equivalences of these calculi is obtained. Further illustrations of FuTS semantics are discussed for deterministically (discrete) timed process algebras and Markov Automata.File | Dimensione | Formato | |
---|---|---|---|
prod_207634-doc_46999.pdf
accesso aperto
Descrizione: Coalgebraic Bisimulation of FuTS
Dimensione
583.74 kB
Formato
Adobe PDF
|
583.74 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.