The Department of Computer Science at the University of Cyprus cordially invites you to the Colloquium entitled:

Parameterised Verification for Multi-Agent Systems


Speaker: Dr. Panagiotis Kouvaros
Affiliation: University of Naples, Italy
Category: Colloquium
Location: Room 148, Faculty of Pure and Applied Sciences (FST-01), 1 University Avenue, 2109 Nicosia, Cyprus (directions)
Date: Wednesday, March 29, 2017
Time: 12:00-13:00 EET
Host: Antonis Kakas (

Recent advances in artificial intelligence have enabled the development and deployment of multi-agent systems and autonomous systems (MAS) in areas of societal importance. However the lack of formal guarantees on their behaviour hinders their adoption by society. To alleviate this problem in the past ten years several methods have been put forward for the efficient model checking of MAS against specifications pertaining to high level attitudes of agency. In this talk I will give a summary account of model checking MAS. I will argue that the model checking problem is intractable for systems of many agents, and therefore not applicable to systems where the number of agents is not known at design time. This is a particularly important class of unbounded MAS, developed in diverse applications ranging from multi-party negotiation and auctions to robotic swarms and scenarios in the internet of things. Accounting for common communication patterns I will introduce a semantics and a specification language to model unbounded MAS and their properties. On this formal setting I will present parameterised model checking techniques for their validation irrespective of the number of agents present. Finally I will discuss an application to the emergence identification problem of robotic swarms and experimental results obtained on MCMAS-P, a tool realising these techniques.

Short Bio:
Panagiotis Kouvaros is a Research Associate in the Department of Computer Science at the University of Naples "Federico ||". Panagiotis works within the formal methods group led my Aniello Muranno on logics and games for imperfect information in multi-agent systems. Previously, he held an EPSRC doctoral prize fellowship in the Department of Computing at Imperial College London. Under the fellowship Panagiotis devised and implemented automated verification methodologies for robotic swarm systems. He was awarded the prize in recognition of his PhD work on the parameterised verification of multi-agent systems carried out in the same department under the supervision of Alessio Lomuscio.

  Mailing List:

Sponsor: The CS Colloquium Series is supported by a generous donation from Microsoft