Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
SMT-based Safety Checking of Parameterized Multi-Agent Systems
Authors: Paolo Felli, Alessandro Gianola, Marco Montali6321-6330
AAAI 2021 | Venue PDF | 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 EMAIL |
| 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. |