A uniform framework for timed automata

Tomasz Brengos, Marco Peressotti

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Timed automata, and machines alike, currently lack a general mathematical characterisation. In this paper we provide a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Key to this work is the use of lax functors for they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems: the index category encodes "how step sequences form executions" (e.g. whether steps duration get accumulated or kept distinct) whereas the base category encodes "step nature and composition" (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.

Original languageEnglish
Title of host publication27th International Conference on Concurrency Theory, CONCUR 2016
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date1. Aug 2016
Article number26
ISBN (Electronic)9783959770170
Publication statusPublished - 1. Aug 2016
Externally publishedYes
Event27th International Conference on Concurrency Theory, CONCUR 2016 - Quebec City, Canada
Duration: 23. Aug 201626. Aug 2016


Conference27th International Conference on Concurrency Theory, CONCUR 2016
CityQuebec City


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


Dive into the research topics of 'A uniform framework for timed automata'. Together they form a unique fingerprint.

Cite this