Skip to main content

2000 | OriginalPaper | Buchkapitel

The Impressive Power of Stopwatches

verfasst von : Franck Cassez, Kim Larsen

Erschienen in: CONCUR 2000 — Concurrency Theory

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

In this paper we define and study the class of stopwatch automata which are timed automata augmented with stopwatches and unobservable 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.

Metadaten
Titel
The Impressive Power of Stopwatches
verfasst von
Franck Cassez
Kim Larsen
Copyright-Jahr
2000
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-44618-4_12