Verification of Multiagent Systems

When and where

Date Hour Room
22 June 2015 10:00-11:20 EG306

Registration form

You can register for the workshop using the online registration form. Registration closes on June 19st June 21st, at 18:00.


Matei Popovici


Multiagent systems (MAS) are often perceived as an architectural paradigm for distributed systems. However, MAS can be used as models for open systems. In such a system, the interacting components are heterogeneous: they may be software pertaining to different organisations or humans.

Verifying properties of such systems is essential for their safe deployment.

In this talk, we shall start from logics for program verification (e.g. Computation-Tree Logic) and show how they can be extended in order to express properties of Multiagent systems. The extension — Alternating-Time Temporal Logic, is a well-known logic for MAS verification.


  1. Brief intro:
    • What is a Multiagent System?
    • What does it mean to specify/verify properties of (arbitrary) systems, and why is this important?
  2. Logics for program verification:
    • Specifying possibility and certainty on transition systems: Modal Logic (ML).
    • Properties of execution sequences (or traces): Linear-Time Temporal Logic (LTL).
    • Quantifying over execution sequences, and expressing (conditional) eventuality: Computation-Tree Logic (CTL).
  3. Logics for Multiagent Systems:
    • From transition systems to games.
    • Specifying strategic abilities (of agents): Alternating-Time Temporal Logics (ATL).
    • Semantic variants of ATL: perfect/imperfect information and recall.


  • Open mindedness
  • Some basic background in propositional logics helps, but is not mandatory


sesiuni/multiagent-systems.txt · Last modified: 2015/06/22 13:50 by fbratiloveanu