Computer Science – Computer Science and Game Theory
Scientific paper
2011-06-07
EPTCS 54, 2011, pp. 146-161
Computer Science
Computer Science and Game Theory
In Proceedings GandALF 2011, arXiv:1106.0814
Scientific paper
10.4204/EPTCS.54.11
We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as "PLTL" by Alur et al. and (in a different version called "PROMPT-LTL") by Kupferman et al.. We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.
No associations
LandOfFree
Optimal Bounds in Parametric LTL Games does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Optimal Bounds in Parametric LTL Games, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Optimal Bounds in Parametric LTL Games will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-25279