Francesco Belardinelli
Tutorial on 2/6/15, 13h30 and 3/6/15, 11h30: Model Checking Multi-agent Systems
Multi-agent systems are open, distributed systems where the processes,
or agents, show highly flexible and autonomous behaviours. The
framework of MAS has been successfully applied to system modelling in
areas as diverse as robotics, security, avionics, e-commerce, and web
services. However, for the effective deployment of multi-agent
technologies, it is fundamental to tackle the verification and
validation questions pertaining to MAS: given a requirement P and a
multi-agent system S, is it the case that S satisfies P? To answer
such questions, in recent years model checkers for MAS have appeared,
thus allowing for the verification of sophisticated MAS scenarios. In
this tutorial I am going to introduce Interpreted Systems [Fagin et
al., Reasoning about Knowledge, MIT, 1995], an established formal
setting for multi-agent systems, together with CTLK, a temporal
epistemic logic for specifying MAS properties. Finally, I will
present MCMAS, a model checking tool currently maintained by the VAS
(Verification of Autonomous Systems) group at Imperial College, which
can be used to verify specification in CTLK on Interpreted Systems.
Talk on 3/6/15, 16h30: A Logic of Knowledge and Strategies with Imperfect Information
Abstract. In this talk we will introduce Epistemic Strategy Logic
(ESL), a logic of knowledge and strategies in contexts of imperfect
information. ESL extends Strategy Logic by adding modal operators for
individual and collective knowledge. This enhanced framework allows
us to represent explicitly and to reason about the knowledge agents
have of their own and other agents’ strategies. We provide a semantics
to ESL in terms of epistemic concurrent game models, then illustrate
the expressive power of ESL as a specification language for games,
both of perfect and imperfect information. Notably, we show that some
fixed-point characterisations of operators for strategic abilities,
which normally fail in contexts of imperfect information, can be
recovered in a controlled way through the interplay of epistemic and
strategy modalities.