Advances in Verification of Multi-agent Systems

Alessio Lomuscio

► To cite this version:

Alessio Lomuscio. Advances in Verification of Multi-agent Systems. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.3-4, 10.1007/978-3-319-72044-9_1 . hal-01767478

HAL Id: hal-01767478

https://inria.hal.science/hal-01767478

Submitted on 16 Apr 2018

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Advances in Verification of Multi-Agent Systems

Alessio Lomuscio

Department of Computing, Imperial College London, UK

**Abstract.** I was honoured by the opportunity to share with the WADT 2016 attendees some of the recent work in our lab on verifying multi-agent systems (MAS) against agent-based specifications.

MAS are distributed autonomous systems in which the components, or agents, act autonomously in order to reach private or common goals. MAS have been used as a paradigm to realise a wide number of applications ranging from autonomous systems and robotics to services, electronic assistants, and beyond. Logic-based specifications for MAS typically do not refer only to the agents’ temporal evolution, but also to their knowledge, strategic abilities, and other AI-inspired primitives.

I began by reporting algorithms for symbolic model checking against episodic and strategic specifications [1, 2]. I highlighted potential speedups of these techniques via a number of techniques including symmetry reduction [3], parallel approaches [4], and SAT-based methods [5].

I then demonstrated MCMAS [6, 7], an open-source BDD-based model checker supporting these specification languages. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicle was discussed [8, 9] as well applications to the verification of artifact-based services [10, 11].

I concluded by considering the case of MAS where the number of agents is unbounded and cannot be determined at design time. This is a typical assumption in robotic swarms and recent internet of things applications. In view of solving this, I reported our approach to the parameterised model checking problem. While this is generally undecidable, I presented results that establish sufficient conditions for determining a *cut-off* of a MAS [12–14], i.e., the number of agents that need to analysed for verifying a MAS composed of any number of components. I concluded by presenting applications to the verification of related notions, such as emergence [15–17].

**Acknowledgements:** The work presented in this talk was partly funded by the EPSRC Research Project "Trusted Autonomous Systems".

**References**

1. Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic **5**(2) (2005) 235–251

2. Cermák, P., Lomuscio, A., Mogavero, F., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15), AAAI Press (2015) 2038–2044
3. Cohen, M., Dam, M., Lomuscio, A., Qu, H.: A symmetry reduction technique for model checking temporal-epistemic logic. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI09). (2009) 721–726

4. Kwiatkowska, M., Lomuscio, A., Qu, H.: Parallel model checking for temporal epistemic logic. In: Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10), IOS Press (2010) 543–548

5. Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae **63**(2-3) (2004) 221–240

6. Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. Software Tools for Technology Transfer **19**(1) (2017) 9–30

7. Cermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: A model checker for the verification of strategy logic specifications. In: Proceedings of the 26th International Conference on Computer Aided Verification (CAV14). Volume 8559 of Lecture Notes in Computer Science., Springer (2014) 525–532

8. Ezekiel, J., Lomuscio, A., Molnar, L., Veres, S.: Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11), AAAI Press (2011) 1659–1664

9. Ezekiel, J., Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems. Information and Computation **254**(2) (2017) 167–194

10. Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verification of GSM-based artifact-centric systems by predicate abstraction. In: Proceedings of the 13th International Conference on Service Oriented Computing (ICSOC15). Volume 9435 of Lecture Notes in Computer Science., Springer (2015) 253–268

11. Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying GSM-based business artifacts. In: Proceedings of the 19th International Conference on Web Services (ICWS12), IEEE Press (2012) 25–32

12. Kouvaros, P., Lomuscio, A.: Automatic verification of parametrised interleaved multi-agent systems. In: Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS13), IFAAMAS (2013) 861–868

13. Kouvaros, P., Lomuscio, A.: A cutoff technique for the verification of parameterised interpreted systems with parameterised environments. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13), AAAI Press (2013) 2013–2019

14. Kouvaros, P., Lomuscio, A.: Parameterised verification for multi-agent systems. Artificial Intelligence **234** (2016) 152–189

15. Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15), AAAI Press (2015) 2081–2088

16. Kouvaros, P., Lomuscio, A.: Verifying emergent properties of swarms. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI15), AAAI Press (2015) 1083–1089

17. Kouvaros, P., Lomuscio, A.: Formal verification of opinion formation in swarms. In: Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS16), IFAAMAS (2016) 1200–1209