Modal Logic for Strategic Reasoning in AI

Module aims

The overall aim of this course is to develop intellectual and practical skills in the use of modal logics for knowledge representation and automated reasoning in Artificial Intelligence.
The first part of the course 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 is meant to lay the foundations of the specification of strategic behaviours of agents in multi-agent systems (MAS), which will be covered in the second part. We will introduce the language of Alternating-time Temporal Logic (ATL), an extension of the temporal logics CTL and LTL, which allows to express game-theoretical notions such as the existence of a winning strategy for a group of agents.
Along the lectures we 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. The students will learn the consequences in terms of valid/satisfiable formulas of these modelling assumptions, as well as will become capable of recognising in what cases these different modeling choices are appropriate given a particular MAS scenario.
Moreover, we will investigate 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.

Recommended: Familiarity with propositional logic and classic first-order predicate logic, e.g. the contents of Discrete mathematics, Logic and Reasoning (JMC: Logic And Reasoning). Systems Verification is useful, but not essential.

Learning outcomes

At the end of this course the students will acquire the ability to

1. Recognise and demonstrate understanding of the distinctive features of modal operators.
2. Understand and recall the definitions of the logics and logical systems presented in the course, and the ideas of the main proofs.
3. Appreciate the differences in the various logics, and their expressive power and limitations.
4. Model concrete examples of multi-agent systems (MAS) by using the framework of concurrent game structures.
5. 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.
6. 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.
7. Apply the model checking algorithms underpinning the verification of ATL properties in concurrent game structures.

Module syllabus

The overall structure of the course can be outlined as follows:

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

Teaching methods

7 weeks of 3 hours of lecture + 1 hours of tutorial
End of course wrap up and revision lectures (2 hours)

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

Assessments

On week 2 and 4 we will give the students a sheet containing exercises slightly more challenging compared to the tutorials, which basically require some research in the provided references. Students will have two weeks to complete each coursework, but our target is that each sheet can be completed in a single week. They will be allowed to work in pairs. This is intended to make sure that everyone is keeping pace with the course, and to give the students regular feedback about their progress.

Each coursework will be submitted through CATe.
Submissions will subsequently be marked by TAs.
Our aim is to return each marked coursework within two weeks.
This should be achievable with the course leaders plus a single TAs.

Module leaders

Dr Francesco Belardinelli