Verifying Fault-tolerance in Parameterised Multi-Agent Systems
Authors: Panagiotis Kouvaros, Alessio Lomuscio
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present an implementation and a case study identifying the threshold under which the alpha swarm aggregation algorithm is robust to faults against its temporal-epistemic specifications. |
| Researcher Affiliation | Academia | Panagiotis Kouvaros Department of Computing Imperial College London, UK University of Naples Federico II , Italy p.kouvaros@imperial.ac.uk Alessio Lomuscio Department of Computing Imperial College London, UK a.lomuscio@imperial.ac.uk |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | No | We developed MCMAS-PFI, a toolkit realising the fault injection method described earlier, on top of MCMAS-P, an opensource model checker for the verification of PIISs [Kouvaros and Lomuscio, 2013]. The paper states MCMAS-P is open-source, but does not provide a direct link or explicit statement that MCMAS-PFI or the specific code for this paper's methodology is open-source or available. |
| Open Datasets | No | We adopt the typical setting employed to analyse the algorithm [Dixon et al., 2012]. In particular we assume that each robot moves on a two-dimensional arena and communicates with its peers via a wireless sensor of limited range. The arena is assumed to be finite and allowed to wrap around, i.e., for an α × α arena, the cell (1, 1) is to the right of the cell (1, α). [...] In the following we fix a 5 × 5 arena, assume a communication range of 1, and let α = 2. Initially the robots are connected, in forward mode, and collectively have every possible direction of movement. We refer to [Kouvaros and Lomuscio, 2015b] for the formal account of the PIISs modelling this instantiation of the algorithm. This describes the simulation setup, not a public dataset. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce the data partitioning. |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types with speeds, memory amounts, or detailed computer specifications) used for running its experiments. |
| Software Dependencies | No | We developed MCMAS-PFI, a toolkit realising the fault injection method described earlier, on top of MCMAS-P, an opensource model checker for the verification of PIISs [Kouvaros and Lomuscio, 2013]. Specific version numbers for MCMAS-P or other software are not provided. |
| Experiment Setup | Yes | In the following we fix a 5 × 5 arena, assume a communication range of 1, and let α = 2. Initially the robots are connected, in forward mode, and collectively have every possible direction of movement. |