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.

Organizers

Matei Popovici

E-mail: pdmatei@gmail.com

Introduction

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.

Topics

Brief intro:
- What is a Multiagent System?
- What does it mean to specify/verify properties of (arbitrary) systems, and why is this important?
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).
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.