Zimmermann, Martin 
ORCID: 0000-0002-8038-2453
(2013)
Optimal bounds in parametric LTL games.
THEORETICAL COMPUTER SCIENCE, 493.
pp. 30-45.
|
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 |
Dimensions
Dimensions
