Satisfiability in a logic of games

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