## Parametric Real-Time Reasoning

*Rajeev Alur,
Thomas A. Henzinger,
and Moshe Y. Vardi*

Traditional approaches to the algorithmic verification of real-time
systems are limited to checking program correctness with respect to
concrete timing properties (e.g., "message delivery within 10
milliseconds"). We address the more realistic and more ambitious
problem of deriving symbolic constraints on the timing properties
required of real-time systems (e.g., "message delivery within the time
it takes to execute two assignment statements"). To model this
problem, we introduce *parametric* timed automata--finite-state
machines whose transitions are constrained with parametric timing
requirements.

The emptiness question for parametric timed automata is central to the
verification problem. On the negative side, we show that in general
this question is undecidable. On the positive side, we provide
algorithms for checking the emptiness of restricted classes of
parametric timed automata. The practical relevance of these classes
is illustrated with several verification examples. There remains a
gap between the automata classes for which we know that emptiness is
decidable and undecidable, respectively, and this gap is related to
various hard and open problems of logic and automata theory.

*Proceedings of the
25th Annual Symposium on Theory of Computing*
(STOC), ACM Press, 1993, pp. 592-601.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1993 ACM.