Parametric Temporal Logic for "Model Measuring"

Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron Peled

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 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 ϕ(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 ε, 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.
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication26th International Colloquium, ICALP'99, Prague, Czech Republic, July 11-15, 1999, Proceedings
PublisherSpringer Berlin Heidelberg
Pages159-168
Number of pages10
Volume1644
ISBN (Electronic)978-3-540-48523-0
ISBN (Print)978-3-540-66224-2
DOIs
Publication statusPublished - 1999

Fingerprint

Dive into the research topics of 'Parametric Temporal Logic for "Model Measuring"'. Together they form a unique fingerprint.

Cite this