Behavioural equivalences for timed systems

Tomasz Brengos, Marco Peressotti

Research output: Working paperResearch

Abstract

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.
Original languageEnglish
Number of pages41
Publication statusPublished - 28. Nov 2017

Keywords

  • Timed automata
  • Semantics
  • Formal methods
  • Quantitative methods
  • Quantitative models
  • Behavioural theory
  • Weak behavioural equivalences
  • Coalgebraic semantics
  • Process calculi
  • Programming Languages
  • Coinduction

Fingerprint

Dive into the research topics of 'Behavioural equivalences for timed systems'. Together they form a unique fingerprint.

Cite this