Optimal Bounds in Parametric LTL Games
Martin Zimmermann
Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables that bound their scope. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of such optimal variable valuations.
Theoretical Computer Science (TCS).
Copyright by Elsevier