The impressive power of stopwatches

Franck Cassez, Kim Larsen

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

139 Citations (Scopus)


In this paper we define and study the class of stopwatch automata which are timed automata augmented with stopwatches and un-observable behaviour. In particular, we investigate the expressive power of this class of automata, and show as a main result that any finite or infinite timed language accepted by a linear hybrid automaton is also acceptable by a stopwatch automaton. The consequences of this result are two-fold: firstly, it shows that the seemingly minor upgrade from timed automata to stopwatch automata immediately yields the full expressive power of linear hybrid automata. Secondly, reachability analysis of linear hybrid automata may effectively be reduced to reachability analysis of stopwatch automata. This, in turn, may be carried out using an easy (over-approximating) extension of the efficient reachability analysis for timed automata to stopwatch automata. We report on preliminary experiments on analyzing translations of linear hybrid automata using a stopwatch-extension of the real-time verification tool UPPAAL.

Original languageEnglish
Title of host publicationCONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings
Place of PublicationBerlin; Heidelberg
Number of pages15
Volume1877 LNCS
Publication statusPublished - 2000
Externally publishedYes
Event11th International Conference on Concurrency Theory, CONCUR 2000 - University Park, PA, United States
Duration: 22 Aug 200025 Aug 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1877 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


Other11th International Conference on Concurrency Theory, CONCUR 2000
Country/TerritoryUnited States
CityUniversity Park, PA


Dive into the research topics of 'The impressive power of stopwatches'. Together they form a unique fingerprint.

Cite this