Abstract
M.Sc. (Mathematics)
This dissertation describes the solution toa specific logical problem, the satisfiability
problem, in a logic of games called Alternating-time Temporal Logic (ATL).
Computation Tree Logic (CTL) is a discrete branching-time temporal logic for reasoning about labelled transition systems. ATL extends CTL to describe gametheoretic situations, where multiple agents together determine the evolution of the system. In particular, ATL explicitly provides for describing the abilities of coalitions of agents in such systems.
Weprovide an automata-based decision procedure for ATL by translating the satisfiability
problem for an ATL formula to the nonemptiness problem for an Alternating
Biichi 'free Automaton. The key result that enables this translation is a oundedbranching
tree model theorem for ATL, proving that a satisfiable formula is also satisfiable
in a tree model of bounded branching degree. In terms of complexity, we show that satisfiability in ATL is complete for exponential time, which agrees with the corresponding complexity result for the fragment CTL.
Closely related to ATL is an independently developed family of modal logics, the
Coalition Logics. The presented results also provide a satisfiability procedure for
Extended Coalition Logic interpreted over strongly playable coalition models.
The structure of the dissertation is as follows:
• Chapter 1 is an introduction to the topic, provides an overview of the results
and a preview of the dissertation.
• Chapter 2 presents some mathematical preliminaries regarding trees, automata,
fixed points and game theory.
• Chapter 3 discusses CTL and in particular an automata-based satisfiability procedure
for CTL.
• Chapter 4 introduces Alternating-time Temporal Logic (ATL) as a logic of games.
• Chapter 5 contains the main results of the dissertation: first we prove a boundedbranching
tree model property for ATL. Then the construction of the required
automaton for satisfiability checking is described.
• Chapter 6 relates the present work to some other logics of games, and in particular
the Coalition Logics.
• Chapter 7 finalises the dissertation with a conclusion and a look at some future
research directions that might be pursued following the present work.