SMT-based Safety Checking of Parameterized Multi-Agent Systems
Authors: Paolo Felli, Alessandro Gianola, Marco Montali6321-6330
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The textual encoding of the ABS corresponding to the PMAS in the running example is solved by MCMT v.3.0, on a machine with Ubuntu 18.04, 3.60 GHz Intel Core i7-7700 CPU, in 2 minutes and 22 seconds and in 56 seconds respectively using Yices (version 1.0.40) and Z3 (version 4.8.9.0) as background SMT solvers. MCMT correctly reports that the system is unsafe. |
| Researcher Affiliation | Academia | Paolo Felli, Alessandro Gianola, Marco Montali Free University of Bozen-Bolzano, Bolzano, Italy {pfelli,gianola,montali}@inf.unibz.it |
| Pseudocode | Yes | Algorithm 1: backward search BReach(ab(M), φ) |
| Open Source Code | Yes | The implementation is available at (Felli, Gianola, and Montali 2020a). SAFE: the Swarm Safety Detector. www.safeswarms.club. Accessed: 2020-12-15. |
| Open Datasets | No | The paper describes a theoretical framework for verifying parameterized multi-agent systems and uses a conceptual example rather than a publicly available dataset for empirical evaluation. |
| Dataset Splits | No | The paper describes a theoretical framework and its implementation for model checking, which does not involve dataset splits like training, validation, or testing. |
| Hardware Specification | Yes | The textual encoding of the ABS corresponding to the PMAS in the running example is solved by MCMT v.3.0, on a machine with Ubuntu 18.04, 3.60 GHz Intel Core i7-7700 CPU |
| Software Dependencies | Yes | MCMT v.3.0, on a machine with Ubuntu 18.04... using Yices (version 1.0.40) and Z3 (version 4.8.9.0) as background SMT solvers. |
| Experiment Setup | Yes | Each global transition of the PMAS is encoded as a sequence of steps of the AB-PMAS, each specified by a disjunction of transition formulae, ordered by means of an additional global variable Phase used to guide the progression. ... The encoding into MCMT input files matches exactly the reduction from PMASs to AB-PMAS described here. |