Timed automata: Semantics, algorithms and tools

  • Johan Bengtsson
  • , Wang Yi*
  • *Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

653 Scopus citations

Abstract

This chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the concrete and abstract semantics of timed automata (based on transition rules, regions and zones), decision problems, and algorithms for verification. A detailed description on DBM (Difference Bound Matrices) is included, which is the central data structure behind several verification tools for timed systems. As an example, we give a brief introduction to the tool UPPAAL.

Original languageEnglish
Pages (from-to)87-124
Number of pages38
JournalLecture Notes in Computer Science
Volume3098
DOIs
StatePublished - 2004
Externally publishedYes

Fingerprint

Dive into the research topics of 'Timed automata: Semantics, algorithms and tools'. Together they form a unique fingerprint.

Cite this