Satisfiability games for branching-time logics

DOI10.2168/LMCS-9(4:5)2013zbMATH Open1312.03023OpenAlexW2028860036MaRDI QIDQ2851673FDOQ2851673

Authors Oliver Friedmann, Martin Lange, Markus Latte 

Publication date 16 October 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.5165

zbMATH Keywords

automatadecidabilitytemporal logicparity games

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80) Temporal logic (03B44)

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

Recommendations

• Model Checking Games for Branching Time Logics
• Branching time? Pruning time!
• Game over: the foci approach to LTL satisfiability and model checking
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• Deciding full branching time logic

Cited In (11)

• Sublogics of a branching time logic of robustness
• Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
• Model Checking Games for Branching Time Logics
• Branching time, perfect information games, and backward induction
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• Game over: the foci approach to LTL satisfiability and model checking
• Title not available (Why is no real title available?)
• A survey on satisfiability checking for the \(\mu \)-calculus through tree automata
• Branching time? Pruning time!
• Playing games with boxes and diamonds.
• Automata-theoretic decision of timed games

Uses Software

• PGSolver
• CTL-RP

This page was built for publication: Satisfiability games for branching-time logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851673)