Optimal Bounds in Parametric LTL Games
Martin Zimmermann
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.
Second International Symposium on Games, Automata, Logic, and Formal Verification (GandALF 2011).
Note that the proof of Theorem 10 contains an error. The journal version presents a 3EXPTIME algorithm for the optimization problems. See also Chapter 3 of my PhD thesis.