Diego Latella ; Mieke Massink ; Erik P De Vink - Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically

lmcs:1617 - Logical Methods in Computer Science, December 22, 2015, Volume 11, Issue 4 - https://doi.org/10.2168/LMCS-11(4:16)2015
Bisimulation of Labelled State-to-Function Transition Systems CoalgebraicallyArticle

Authors: Diego Latella ORCID; Mieke Massink ORCID; Erik P De Vink

    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.


    Volume: Volume 11, Issue 4
    Published on: December 22, 2015
    Submitted on: September 16, 2015
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours; Funder: European Commission; Code: 600708
    • Autonomic Service-Component Ensembles; Funder: European Commission; Code: 257414

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1000 times.
    This article's PDF has been downloaded 424 times.