Optimal bounds in parametric LTL games



Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2013) Optimal bounds in parametric LTL games. THEORETICAL COMPUTER SCIENCE, 493. pp. 30-45.

[thumbnail of optimalbounds.pdf] Text
optimalbounds.pdf - Author Accepted Manuscript

Download (535kB) | Preview

Abstract

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. © 2013 Elsevier B.V. All rights reserved.

Item Type: Article
Uncontrolled Keywords: Infinite games, Parametric linear temporal logic, PROMPT-LTL, Optimal winning strategies
Depositing User: Symplectic Admin
Date Deposited: 15 Jul 2019 12:49
Last Modified: 19 Jan 2023 00:37
DOI: 10.1016/j.tcs.2012.07.039
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3050014