## 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.

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