Parametric LTL Games
Martin Zimmermann
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.
Technical Report AIB-2010-11, RWTH Aachen University.
Preliminary version of the TCS paper Optimal bounds in Parametric LTL Games, which supersedes the results presented here.