Bisimulation of labelled state-to-function transition systems coalgebraically

DOI10.2168/LMCS-11(4:16)2015MaRDI QIDQ3460420zbMATH OpenOpenAlexFDO

Authors Erik de Vink, Diego Latella, Mieke Massink

Publication date 7 January 2016

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.05866

zbMATH Keywords

coalgebrabisimulationbehavioral equivalencefunction of finite supportFuTSquantitative process algebra

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions 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 coincides with behavioural equivalence of the associated functor. As generic examples, the equivalences underlying substantial fragments of major examples of quantitative process algebras are related to the bisimilarity of specific FuTS. The examples range from a stochastic process language, PEPA, to a language for Interactive Markov Chains, IML, a (discrete) timed process language, TPC, and a language for Markov Automata, MAL. The equivalences underlying these languages are related to the bisimilarity of their specific FuTS. By the correspondence result coalgebraic justification of the equivalences of these calculi is obtained. The specific selection of languages, besides covering a large variety of process interaction models and modelling choices involving quantities, allows us to show different classes of FuTS, namely so-called simple FuTS, combined FuTS, nested FuTS, and general FuTS.

Recommendations

• Bisimulation for probabilistic transition systems: A coalgebraic approach
• Bisimulation for probabilistic transition systems: a coalgebraic approach
• An exercise on transition systems
• Relating coalgebraic notions of bisimulation. With applications to name-passing process calculi (extended abstract)
• Coalgebras for fuzzy transition systems

Cited in

(9)

• Towards general axiomatizations for bisimilarity and trace semantics
• Monoid-labeled transition systems
• Performance preserving equivalence for stochastic process algebra dtsdPBC
• A definition scheme for quantitative bisimulation
• A ground-complete axiomatization of stateless bisimilarity over Linda
• scientific article; zbMATH DE number 6864542 (Why is no real title available?)
• \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
• A Characterisation of Expressivity for Coalgebraic Bisimulation and Simulation
• scientific article; zbMATH DE number 2186713 (Why is no real title available?)

Describes a project that uses

Uses Software

• MarCaSPiS
• MoDeST

This page was built for publication: Bisimulation of labelled state-to-function transition systems coalgebraically

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460420)