*Abstract:*

Every logic comes with several decision
problems. One of them is the *model checking* problem: does a
given structure satisfy a given formula? Another is the
*satisfiability* problem: for a given formula, is there a
structure fulfilling it?

For modal and temporal logics; tableaux, automata and games are commonly accepted as helpful techniques that solve these problems. The fact that these logics possess the tree model property makes tableau structures suitable for these tasks. On the other hand, starting with Büchi's work, intimate connections between these logics and automata have been found. A formula can describe an automaton's behaviour, and automata are constructed to accept exactly the word or tree models of a formula.

In recent years the use of games has become more popular. There, an existential and a universal player play on a formula (and a structure) to decide whether the formula is satisfiable, resp. satisfied. The logical problem at hand is then characterised by the question of whether or not the existential player has a winning strategy for the game. These three methodologies are closely related. For example the non-emptiness test for an alternating automaton is nothing more than a 2-player game, while winning strategies for games are very similar to tableaux.

Game-theoretic characterisations of logical problems give rise to an interactive semantics for the underlying logics. This is particularly useful in the specification and verification of concurrent systems where games can be used to generate counterexamples to failing properties in a very natural way.

We start by defining simple model checking games for Propositional Dynamic Logic, PDL, in Chapter 4. These allow model checking for PDL in linear running time. In fact, they can be obtained from existing model checking games for the alternating free µ-calculus. However, we include them here because of their usefulness in proving correctness of the satisfiability games for PDL later on. Their winning strategies are history-free.

Chapter 5 contains model checking games for
branching time logics. Beginning with the Full Branching Time Logic
CTL^{*} we introduce the notion of a *focus game*. Its
key idea is to equip players with a tool that highlights a
particular formula in a set of formulas. The winning conditions for
these games consider the players' behaviours regarding the change
of the focus. This proves to be useful in capturing the
regeneration of least and greatest fixed point constructs in
CTL^{*}. Deciding the winner of these games can be done
using space which is polynomial in the size of the input. Their
winning strategies are history-free, too.

We also show that model checking games for
CTL^{+} arise from those for CTL^{*} by
disregarding the focus. This does not affect the polynomial space
complexity. These can be further optimised to obtain model checking
games for the Computation Tree Logic CTL which coincide with the
model checking games for the alternating free µ-calculus
applied to formulas translated from CTL into it. This optimisation
improves the games' computational complexity, too. As in the PDL
case, deciding the winner of such a game can be done in linear
running time. The winning strategies remain history-free.

Focus games are also used to give game-based accounts of the satisfiability problem for Linear Time Temporal Logic LTL, CTL and PDL in Chapter 6. They lead to a polynomial space decision procedure for LTL, and exponential time decision procedures for CTL and PDL. Here, winning strategies are only history-free for the existential player. The universal player s strategies depend on a finite part of the history of a play.

In spite of the strong connections between tableaux, automata and games their differences are more than simply a matter of taste. Complete axiomatisations for LTL, CTL and PDL can be extracted from the satisfiability focus games in an elegant way. This is done in Chapter 7 by formulating the game rules, the winning conditions and the winning strategies in terms of an axiom system. Completeness of this system then follows from the fact that the existential player wins the game on a consistent formula, i.e. it is satisfiable.

We also introduce satisfiability games for
CTL^{*} based on the focus approach. They lead to a double
exponential time decision procedure. As in the LTL, CTL and PDL
case, only the existential player has history-free winning
strategies. Since these strategies witness satisfiability of a
formula and stay in close relation to its syntactical structure, it
might be possible to derive a complete axiomatisation for
CTL^{*} from these games as well.

Finally, Chapter 9 deals with Fixed Point Logic with Chop, FLC. It extends modal µ-calculus with a sequential composition operator. Satisfiability for FLC is undecidable but its model checking problem remains decidable. In fact it is hard for polynomial space.

We give two different game-based solutions to the model checking problem for FLC. Deciding the winner for both types of games meets this polynomial space lower bound for formulas with fixed alternation (and sequential) depth. In the general case the winner can be determined using exponential time, resp. exponential space. The former result holds for games that give rise to global model checking whereas the latter describes the complexity of local FLC model checking. FLC is interesting for verification purposes since it --- unlike all the other logics discussed here --– can describe properties which are non-regular.

The thesis concludes with remarks and comments on further research in the area of games for modal and temporal logics.

This report is available in the following formats:

Previous | Index | Next