## Parametric Temporal Logic for Model Measuring

*Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron Peled*
We extend the standard model checking paradigm of
linear temporal logic, LTL, to a ``model measuring'' paradigm
where one can obtain more quantitative information beyond a ``Yes/No''
answer.
For this purpose, we define a {\em parametric temporal logic\/}, PLTL,
which allows statements such as
``a request p is followed in at most x steps
by a response q'',
where x is a free variable. We show how one can, given a
formula phi(x_1, ...x_k) of PLTL
and a system model K,
not only determine whether there exists a
valuation of x_1, ... x_k
under which the system K
satisfies the property phi,
but if so
find valuations which satisfy
various optimality criteria.
In particular, we present algorithms for
finding valuations which
minimize (or maximize) the maximum (or minimum) of all parameters.
These algorithms
exhibit the same PSPACE complexity as LTL model checking.
We show that our choice of syntax for PLTL lies at the threshold of
decidability for parametric temporal logics, in that several
natural extensions have undecidable
``model measuring'' problems.

*Automata, Languages, and Programming:
Proceedings of the 26th International Conference*,
(ICALP'99),
Lecture Notes in Computer Science 1644,
Springer, pp. 159--168, 1999.