Behavioural equivalences for timed systems

Tomasz Brengos, Marco Peressotti

Research output: Contribution to journalJournal articleResearchpeer-review

70 Downloads (Pure)


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
Article number17
JournalLogical Methods in Computer Science
Issue number1
Pages (from-to)17:1-17:41
Number of pages41
Publication statusPublished - 28. Feb 2019


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


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

Cite this