SMT-based Safety Checking of Parameterized Multi-Agent Systems

Authors

  • Paolo Felli Free University of Bozen-Bolzano, Bolzano, Italy
  • Alessandro Gianola Free University of Bozen-Bolzano, Bolzano, Italy
  • Marco Montali Free University of Bozen-Bolzano, Bolzano, Italy

Keywords:

Action, Change, and Causality

Abstract

We study the problem of verifying whether a given parameterized multi-agent system (PMAS) is safe, namely whether none of its possible executions can lead to bad states. These are captured by a state formula existentially quantifying over agents. As the MAS is parameterized, it only describes the finite set of possible agent templates, while the actual number of concrete agent instances that will be present at runtime, for each template, is unbounded and cannot be foreseen. We solve this problem via infinite-state model checking based on satisfiability modulo theories (SMT), relying on the theory of array-based systems. We formally characterize the soundness, completeness and termination guarantees of our approach under specific assumptions. This gives us a technique that is implementable on top of third-party, SMT-based model checkers. Finally, we discuss how this approach lends itself to richer parameterized and data-aware MAS settings beyond the state-of-the-art solutions in the literature.

Downloads

Published

2021-05-18

How to Cite

Felli, P., Gianola, A., & Montali, M. (2021). SMT-based Safety Checking of Parameterized Multi-Agent Systems. Proceedings of the AAAI Conference on Artificial Intelligence, 35(7), 6321-6330. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16785

Issue

Section

AAAI Technical Track on Knowledge Representation and Reasoning