Optimal Bounds in Parametric LTL Games

Martin Zimmermann
(RWTH Aachen University)

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as "PLTL" by Alur et al. and (in a different version called "PROMPT-LTL") by Kupferman et al..

We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.

In Giovanna D'Agostino and Salvatore La Torre: Proceedings Second International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011), Minori, Italy, 15-17th June 2011, Electronic Proceedings in Theoretical Computer Science 54, pp. 146–161.
Published: 4th June 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.54.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org