Abstract

I want to talk about some recent work with Martin Lange, which uses games for understanding satisfiability of temporal logics.

When temporal logics began to be used in Computer Science, satisfiability checking was based on tableaux. However satisfiability for each variant or extension of a temporal logic then required a new hand crafted tableau decision procedure. Often these methods were far from optimal. This prompted the use of automata for deciding satisfiability of temporal formulas. Buchi or Rabin tree automata offer a very useful finite characterisation of the ``infinite'' models of a temporal formula.

However decision procedures for satisfiability based on automata do not fit so well with the issue of finding a sound and complete axiomatisation of a temporal logic. Instead one tries to craft a model out of consistent sets of formulas.

Instead we propose a new basis for satisfiability of temporal logics using two player games, which employ a novel ``focus'' feature. We show that there are very simple focus games for LTL (linear time temporal logic) and CTL (computation tree logic). In both these cases there is a straightforward method for ``reading off'' a complete axiom system for the logics.