Paper: Focus Games for Satisfiability and Completeness of Temporal Logic (at LICS 2001)

Authors: Martin Lange Colin Stirling

Abstract

We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit and transparent, and underpin a novel approach to developing complete axiom systems for temporal logic. The axiom systems are naturally factored into what happens locally and what happens in the limit. The completeness proofs utilise the game theoretic construction for satisfiability: if a finite set of formulas is consistent then there is a winning strategy (and therefore construction of an explicit model is avoided).

BibTeX

  @InProceedings{LangeStirling-FocusGamesforSatisf,
    author = 	 {Martin Lange and Colin Stirling},
    title = 	 {Focus Games for Satisfiability and Completeness of Temporal Logic},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {357--365},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }