Modal Logics for Multi-Agent Systems
Marc Pauly and Michael Wooldridge
Department of Computer Science
University of Liverpool
Liverpool L69 72F, United Kingdom
(pauly@csc.liv.ac.uk) or (mjw@csc.liv.ac.uk)
Prerequisites: The course assumes a basic knowledge of propositional & predicate
logic. Although prior knowledge of modal logics is not required, some
preliminary reading would be advantageous: we recommend the first 3
chapters of ``Reasoning about Knowledge'', by R Fagin, J Y Halpern, Y
Moses, and M Vardi (MIT Press, 1995).
Summary: Modal logics of various kinds have proved to be extremely valuable
formal tools in attempting to understand multi-agent systems. In this
course, we will investigate the use of such logics. We focus on the
use of modal logics as formal specification languages, for
verification and synthesis of multi-agent systems. The course is
divided into four parts.
In part one, we briefly review the foundations of modal, temporal,
and dynamic logics, Kripke semantics, and basic ideas from
correspondence theory. This part sets the technical scene for the
remainder of the course.
In part two, we focus on a particular class of logics for multi-agent
systems, known as belief-desire-intention (BDI) logics. In BDI logics,
we attempt to understand the behaviour of rational agents by
attributing to them attitudes such as believing, desiring, and
intending. Logics with modalities corresponding to these attitudes are
developed, with the goal being to capture the behaviour of a rational
agent when endowed with such attitudes.
In part three, we introduce two game logics developed to capture
cooperation in multi-agent systems. Coalition Logic offers a simple
modal language for expressing what groups of agents can bring about
by joining to form a coalition. Alternating Temporal Logic extends
this basic modal language to capture coalitional power in the long run.
In part four, we investigate the potential applications of multi-agent
logics. We discuss the issues that arise when such logics are used in
the specification and verification of computer systems, and how such
logics might be used to develop and verify social procedures.
Course Notes:
Lecture One PS PDF
Lecture Two PS PDF
Lecture Three PS PDF
Lecture Four PS PDF
Lecture Five PS PDF
Back to course listing.