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 June 2010
Contact Data Privacy Policy Imprint
Home People Publications
More