Optimal Bounds in Parametric LTL Games
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1106.1237v1 |
| _version_ | 1818206464845545472 |
|---|---|
| author | Martin Zimmermann |
| author_facet | Martin Zimmermann |
| author_sort | Martin Zimmermann |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-12T04:13:27Z |
| format | Article |
| id | doaj.art-0edfade236124518a0041e9d71bb3c5c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T04:13:27Z |
| publishDate | 2011-06-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-0edfade236124518a0041e9d71bb3c5c2022-12-22T00:38:33ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-06-0154Proc. GandALF 201114616110.4204/EPTCS.54.11Optimal Bounds in Parametric LTL GamesMartin ZimmermannWe 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.http://arxiv.org/pdf/1106.1237v1 |
| spellingShingle | Martin Zimmermann Optimal Bounds in Parametric LTL Games Electronic Proceedings in Theoretical Computer Science |
| title | Optimal Bounds in Parametric LTL Games |
| title_full | Optimal Bounds in Parametric LTL Games |
| title_fullStr | Optimal Bounds in Parametric LTL Games |
| title_full_unstemmed | Optimal Bounds in Parametric LTL Games |
| title_short | Optimal Bounds in Parametric LTL Games |
| title_sort | optimal bounds in parametric ltl games |
| url | http://arxiv.org/pdf/1106.1237v1 |
| work_keys_str_mv | AT martinzimmermann optimalboundsinparametricltlgames |