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 epistemic 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,13,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,16,17].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. J. Appl. Logic 5(2), 235–251 (2005)
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), pp. 2038–2044. AAAI Press (2015)
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), pp. 721–726 (2009)
Kwiatkowska, M., Lomuscio, A., Qu, H.: Parallel model checking for temporal epistemic logic. In: Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10), pp. 543–548. IOS Press (2010)
Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae 63(2–3), 221–240 (2004)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. Softw. Tools Technolo. Trans. 19(1), 9–30 (2017)
Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525–532. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_34
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), pp. 1659–1664. AAAI Press (2011)
Ezekiel, J., Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems. Inf. Comput. 254(2), 167–194 (2017)
Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verification of GSM-based artifact-centric systems by predicate abstraction. In: Barros, A., Grigori, D., Narendra, N.C., Dam, H.K. (eds.) ICSOC 2015. LNCS, vol. 9435, pp. 253–268. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48616-0_16
Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying GSM-based business artifacts. In: Proceedings of the 19th International Conference on Web Services (ICWS12), pp. 25–32. IEEE Press (2012)
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, pp. 861–868 (2013)
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), pp. 2013–2019. AAAI Press (2013)
Kouvaros, P., Lomuscio, A.: Parameterised verification for multi-agent systems. Artif. Intell. 234, 152–189 (2016)
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), pp. 2081–2088. AAAI Press (2015)
Kouvaros, P., Lomuscio, A.: Verifying emergent properties of swarms. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI15), pp. 1083–1089. AAAI Press (2015)
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, pp. 1200–1209 (2016)
Acknowledgements
The work presented in this talk was partly funded by the EPSRC Research Project “Trusted Autonomous Systems”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 IFIP International Federation for Information Processing
About this paper
Cite this paper
Lomuscio, A. (2017). Advances in Verification of Multi-agent Systems. In: James, P., Roggenbach, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2016. Lecture Notes in Computer Science(), vol 10644. Springer, Cham. https://doi.org/10.1007/978-3-319-72044-9_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-72044-9_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72043-2
Online ISBN: 978-3-319-72044-9
eBook Packages: Computer ScienceComputer Science (R0)