Parametric LTL Games
Martín Zimmermann · RWTH Publications (RWTH Aachen) · 2009
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.. Our work lifts their results on model checking for PLTL and PROMPT-LTL to the level of games: we present algorithms that determine whether a player wins a game with respect to some, infinitely many, or all variable valuations. All these algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games. Furthermore, we show how to determine optimal valuations that allow a player to win a game.