Tomasz Brengos ; Marco Peressotti - Behavioural equivalences for timed systems

lmcs:4104 - Logical Methods in Computer Science, February 28, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:17)2019
Behavioural equivalences for timed systemsArticle

Authors: Tomasz Brengos ; Marco Peressotti ORCID

    Timed transition systems are behavioural models that include an explicit treatment of time flow and are used to formalise the semantics of several foundational process calculi and automata. Despite their relevance, a general mathematical characterisation of timed transition systems and their behavioural theory is still missing. We introduce the first uniform framework for timed behavioural models that encompasses known behavioural equivalences such as timed bisimulations, timed language equivalences as well as their weak and time-abstract counterparts. All these notions of equivalences are naturally organised by their discriminating power in a spectrum. We prove that this result does not depend on the type of the systems under scrutiny: it holds for any generalisation of timed transition system. We instantiate our framework to timed transition systems and their quantitative extensions such as timed probabilistic systems.


    Volume: Volume 15, Issue 1
    Published on: February 28, 2019
    Accepted on: February 11, 2019
    Submitted on: November 29, 2017
    Keywords: Computer Science - Logic in Computer Science,F.1.1

    Consultation statistics

    This page has been seen 1369 times.
    This article's PDF has been downloaded 447 times.