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

lmcs:761 - Logical Methods in Computer Science, October 16, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:5)2013
Satisfiability Games for Branching-Time LogicsArticle

Authors: Oliver Friedmann ; Martin Lange ; Markus Latte

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


    Volume: Volume 9, Issue 4
    Published on: October 16, 2013
    Imported on: February 5, 2013
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Model Checking Unleashed; Funder: European Commission; Code: 259267

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1117 times.
    This article's PDF has been downloaded 425 times.