Verification of Swarm Systems (2012 - 2020)

Motivation

Swarm robotics is an approach to performing a task by using a large number of robots that coordinate to accomplish their common goal. Robotic swarms have been put forward a good alternative to single robots in a number of scenarios including tasks such as surveillance and maintenance of industrial plants.

In safety critical situations, it is necessary to verify that these swarm systems will behave as expected regardless of how many agents are present in the system. However, this cannot be achieved with traditional model checking techniques since it involves checking an unbounded number of systems. This project aims to develop novel model checking techniques that enable the verification of these unbounded multi-agent systems.

Objectives and current results

To enable the development of verification methods, the project aims at defining semantic models and formal specification languages for swarm systems.

A number of such semantics have been proposed, both for modelling synchronous systems (in which all the participants perform actions simultaneously) and asychronous systems (where participants may perform actions independently). Both non-deterministic and stochastic semantics have been considered, and formal specification languages have been explored ranging from those describing simple temporal properties to richer logics that can describe probabilistic, epistemic, or strategic properties.

These techniques have also been extended to address the verification of faulty systems (where the participants in the swarm may exhibit faults) and open systems (where participants of the swarm may leave or join at run-time).

More details on our current research can be found in the Software and Publications sections below.

Software

The following tools have been developed within the project:

  • A number of extensions to MCMAS to enable the verification of non-probabilistic unbounded multi-agent systems. These can be found here.
  • A number of variants of PSV (Probabilistic Swarm Verifier), which are built on top of PRISM and enable the verification of unbounded probabilistic multi-agent systems. These can be found here.

Publications

A. Lomuscio, E. Pirovano.
Verifying Fault-Tolerance in Probabilistic Swarm Systems.
Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI20). Yokohama, Japan. AAAI Press.

A. Lomuscio, E. Pirovano.
Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems.
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.

P. Kouvaros, A. Lomuscio, E. Pirovano, H. Punchihewa.
Formal Verification of Open Multi-Agent Systems
Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.

A. Lomuscio, E. Pirovano.
A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems
Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.

P. Kouvaros, A. Lomuscio, E. Pirovano.
Symbolic Synthesis of Fault-Tolerance Ratios in Parameterised Multi-Agent Systems
Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.

A. Lomuscio, E. Pirovano.
Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems
Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.

P. Kouvaros, A. Lomuscio.
Towards the Formal Verification of Correctness and Robustness of Robot Swarms (Invited Talk).
Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic.

P. Kouvaros, A. Lomuscio.
Verifying Fault-tolerance in Parameterised Multi-Agent Systems
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 288-294. AAAI Press.

F. Belardinelli, P. Kouvaros, A. Lomuscio.
Parameterised Verification of Data-aware Multi-agent Systems.
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. pp 98-104. AAAI Press.

P. Kouvaros, A. Lomuscio.
Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction
Proceedings of the 31th AAAI Conference on Artificial Intelligence (AAAI17). San Francisco (CA), USA. pp 3013-3020. AAAI Press.

P. Kouvaros, A. Lomuscio.
Parameterised Model Checking for Alternating-time Temporal Logic
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.

P. Kouvaros, A. Lomuscio.
Formal Verification of Opinion Formation in Swarms
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.

I. Boureanu, P. Kouvaros, A. Lomuscio.
Verifying Security Properties in Unbounded Multiagent Systems
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.

P. Kouvaros, A. Lomuscio.
Parameterised Verification for Multi-Agent Systems
Artificial Intelligence. Elsevier.

P. Kouvaros, A. Lomuscio.
Verifying Emergent Properties of Swarms
Proceedings of the Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15). Buonos Aires, Argentina. AAAI Press.

P. Kouvaros, A. Lomuscio.
A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). pp 2013-2019. AAAI Press.

P. Kouvaros, A. Lomuscio.
Automatic Verification of Parametrised Interleaved Multi-Agent Systems
Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS13). Saint Paul, MN, USA. pp 861-868. IFAAMAS Press.

Team members

Principal investigator
Research associates
Collaborators

Funding

This research is supported by a Royal Academy of Engineering Chair in Emerging Technologies and an EPSRC-sponsored studentship.

It was previously also supported by an EPSRC fellowship on Trusted Autonomous Systems.