Friedmann, Oliver and Lange, Martin and Latte, Markus - Satisfiability Games for Branching-Time Logics

lmcs:761 - Logical Methods in Computer Science, October 16, 2013, Volume 9, Issue 4
Satisfiability Games for Branching-Time Logics

Authors: Friedmann, Oliver and Lange, Martin and Latte, Markus

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+.


Source : oai:arXiv.org:1308.5165
DOI : 10.2168/LMCS-9(4:5)2013
Volume: Volume 9, Issue 4
Published on: October 16, 2013
Submitted on: February 5, 2013
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 96 times.
This article's PDF has been downloaded 122 times.