Satisfiability Games for Branching-Time Logics
The satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational complexities are known: CTL* and CTL+ are complete for doubly exponential time, CTL is complete for single exponential time....
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/761/pdf |
| _version_ | 1797268735245942784 |
|---|---|
| author | Oliver Friedmann Martin Lange Markus Latte |
| author_facet | Oliver Friedmann Martin Lange Markus Latte |
| author_sort | Oliver Friedmann |
| collection | DOAJ |
| description | The satisfiability problem for branching-time temporal logics like CTL*, CTL
and CTL+ has important applications in program specification and verification.
Their computational complexities are known: CTL* and CTL+ are complete for
doubly exponential time, CTL is complete for single exponential time. Some
decision procedures for these logics are known; they use tree automata,
tableaux or axiom systems. In this paper we present a uniform game-theoretic
framework for the satisfiability problem of these branching-time temporal
logics. We define satisfiability games for the full branching-time temporal
logic CTL* using a high-level definition of winning condition that captures the
essence of well-foundedness of least fixpoint unfoldings. These winning
conditions form formal languages of \omega-words. We analyse which kinds of
deterministic {\omega}-automata are needed in which case in order to recognise
these languages. We then obtain a reduction to the problem of solving parity or
B\"uchi games. The worst-case complexity of the obtained algorithms matches the
known lower bounds for these logics. This approach provides a uniform, yet
complexity-theoretically optimal treatment of satisfiability for branching-time
temporal logics. It separates the use of temporal logic machinery from the use
of automata thus preserving a syntactical relationship between the input
formula and the object that represents satisfiability, i.e. a winning strategy
in a parity or B\"uchi game. The games presented here work on a Fischer-Ladner
closure of the input formula only. Last but not least, the games presented here
come with an attempt at providing tool support for the satisfiability problem
of complex branching-time logics like CTL* and CTL+. |
| first_indexed | 2024-04-25T01:37:12Z |
| format | Article |
| id | doaj.art-f1f13180a1ec4c5c818fcb5b40f1990a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:12Z |
| publishDate | 2013-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-f1f13180a1ec4c5c818fcb5b40f1990a2024-03-08T09:30:37ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-10-01Volume 9, Issue 410.2168/LMCS-9(4:5)2013761Satisfiability Games for Branching-Time LogicsOliver FriedmannMartin LangeMarkus LatteThe satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational complexities are known: CTL* and CTL+ are complete for doubly exponential time, CTL is complete for single exponential time. Some decision procedures for these logics are known; they use tree automata, tableaux or axiom systems. In this paper we present a uniform game-theoretic framework for the satisfiability problem of these branching-time temporal logics. We define satisfiability games for the full branching-time temporal logic CTL* using a high-level definition of winning condition that captures the essence of well-foundedness of least fixpoint unfoldings. These winning conditions form formal languages of \omega-words. We analyse which kinds of deterministic {\omega}-automata are needed in which case in order to recognise these languages. We then obtain a reduction to the problem of solving parity or B\"uchi games. The worst-case complexity of the obtained algorithms matches the known lower bounds for these logics. This approach provides a uniform, yet complexity-theoretically optimal treatment of satisfiability for branching-time temporal logics. It separates the use of temporal logic machinery from the use of automata thus preserving a syntactical relationship between the input formula and the object that represents satisfiability, i.e. a winning strategy in a parity or B\"uchi game. The games presented here work on a Fischer-Ladner closure of the input formula only. Last but not least, the games presented here come with an attempt at providing tool support for the satisfiability problem of complex branching-time logics like CTL* and CTL+.https://lmcs.episciences.org/761/pdfcomputer science - logic in computer science |
| spellingShingle | Oliver Friedmann Martin Lange Markus Latte Satisfiability Games for Branching-Time Logics Logical Methods in Computer Science computer science - logic in computer science |
| title | Satisfiability Games for Branching-Time Logics |
| title_full | Satisfiability Games for Branching-Time Logics |
| title_fullStr | Satisfiability Games for Branching-Time Logics |
| title_full_unstemmed | Satisfiability Games for Branching-Time Logics |
| title_short | Satisfiability Games for Branching-Time Logics |
| title_sort | satisfiability games for branching time logics |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/761/pdf |
| work_keys_str_mv | AT oliverfriedmann satisfiabilitygamesforbranchingtimelogics AT martinlange satisfiabilitygamesforbranchingtimelogics AT markuslatte satisfiabilitygamesforbranchingtimelogics |