Modal Logic for Strategic Reasoning

Module aims

The overall aim of this module is to develop your intellectual and practical skills in the use of modal logics for knowledge representation and automated reasoning in Artificial Intelligence.
In the first part of the module we will focus on general modal logic: modal and temporal operators, Kripke frames and models, and the basics of the model theory of modal logics, including the notions of satisfaction and validity, their computational complexity, as well as invariance under bisimulation.  This part gives you the foundations for the specification of strategic behaviours of agents in multi-agent systems (MAS), which you will study in the second part.
In this second part, you are introduced to the language of Alternating-time Temporal Logic (ATL), an extension of the temporal logics CTL and LTL, which will allow you to express game-theoretical notions such as the existence of a winning strategy for a group of agents.
You will analyse the various assumptions that can be made about the reasoning capabilities of autonomous agents: agents can have perfect observability on the environment in which they are interacting with the other agents, or they might only have partial observability; they might remember all the sequence of events leading to their current state, or their memory might be limited in some way. You will learn the consequences, in terms of valid/satisfiable formulas, of these modelling assumptions; and you will become capable of recognising in what cases these different modeling choices are appropriate given a particular MAS scenario.
You will also see how the complexity of the model checking problem for ATL depends on these modeling choices. Model checking algorithms will be illustrated for all cases in which the problem is decidable, while undecidable cases will also be explained briefly.

Learning outcomes

At the end of this module, you will acquire the ability to
• Recognise and demonstrate understanding of the distinctive features of modal operators.
• Recall and present the definitions of the logics and logical systems presented in the module, and the ideas of the main proofs.
• Specify the differences in the various logics, and their expressive power and limitations.
• Model concrete examples of multi-agent systems (MAS) by using the framework of concurrent game structures.
• Translate informal specifications of strategic abilities of agents in MAS, expressed in the English language, into formulas of temporal logics LTL and CTL, and Alternating-time Temporal Logic ATL.
• Recognise the differences in modeling agents having perfect/imperfect information about the environment and the other agents, as well as agents having perfect/imperfect recall of past events.
• Apply the model checking algorithms underpinning the verification of ATL properties in concurrent game structures.

Module syllabus

The overall structure of the module can be outlined as follows:
1. Basic Concepts
a. Modal Languages; b. Kripke Models and Frames; c. Modal Consequence Relations, Decision Problems, Validity; d. Normal Modal Logics
2. Models
a. Invariance Results, Bisimulations; b. Standard Translation; c. Characterization and Definability; d. Simulation and Safety
3. Frames
a. Frame Definability and Second-Order Logic; b. Definable and Undefinable Properties; c.Finite Frames; d. Automatic First-Order Correspondence
4. Reasoning about Systems
a. Multi-Agent Systems; b. The Role of Logics for MAS; c. Formal Verification;
5. Reasoning about Time and Change
a. Temporal Logics; b. Linear Temporal Logic (LTL); c. Computation Tree Logic (CTL); d. Complexity of Model Checking Temporal Logics
6. Reasoning about Strategic Abilities
a. Concurrent Game Structures; b. Alternating-Time Temporal Logic; c. Agents, Systems, Games;
7. Verification of Strategic Ability
a. Properties of Alternating-time Temporal Logic (validity and satisfiability problems); b. Model Checking ATL; c.    Model Checking ATL*
8. Abilities under Imperfect Information
a. Strategies and Knowledge; b. Properties of ATL under imperfect information (validity and satisfiability problems); c. The Subjective Interpretation

Teaching methods

The material will be taught through lectures, backed up by unassessed, formative exercises designed to reinforce the material as it is taught.  Assessed coursework is designed in order to make sure that everyone is keeping pace with the module, and to give you regular feedback about your progress.

An online service will be used as an open discussion forum for the module.

Assessments

There will be two pieces of assessed coursework, worth 10% each, and each containing written exercises.  These will require some research in the provided references; you may complete them in pairs.  There will be a final written examination worth 80%.  Tutorial exercises will be similar in style to those of the coursework and final examination.

Written feedback will be provided for the assessed coursework.  Feedback on the formative exercises will be given verbally, in class.               
 

Module leaders

Dr Francesco Belardinelli