Verifying Fault-Tolerance in Probabilistic Swarm Systems
Authors: Alessio Lomuscio, Edoardo Pirovano
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We outline a verification procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained. To evaluate the usefulness of our tool we consider the swarm foraging protocol [Campo and Dorigo, 2007; Liu and Winfield, 2010] that has previously been verified in a probabilistic setting without any faults in [Lomuscio and Pirovano, 2019]. We extend this analysis to introduce a fault. ... We conducted this analysis and recorded in Figure 2 the maximum p for which the property holds for different values of k and pf. |
| Researcher Affiliation | Academia | Alessio Lomuscio and Edoardo Pirovano Department of Computing, Imperial College London {a.lomuscio, e.pirovano17}@imperial.ac.uk |
| Pseudocode | Yes | Algorithm 1 PFTP Decision Procedure |
| Open Source Code | Yes | The source code for this and the model we consider below are released as open-source [PSV-F, 2020]. |
| Open Datasets | No | The paper analyzes a swarm foraging protocol described in cited works [Campo and Dorigo, 2007; Liu and Winfield, 2010] but does not refer to or provide access to a 'dataset' in the context of training or evaluation data for a machine learning model. The experiments involve verifying properties of a system, not training on a dataset. |
| Dataset Splits | No | The paper describes a formal verification method and experiments, but does not involve machine learning models or traditional dataset splits (training, validation, test). |
| Hardware Specification | No | The paper mentions performance metrics like model construction time and specification checking time (e.g., 'constructing the model took approximately 400 seconds and the specification was checked in approximately 5 seconds'), but it does not specify any hardware details such as CPU, GPU models, or memory. |
| Software Dependencies | Yes | We implemented the method described in the previous sections in a Java toolkit called PSV-F (Probabilistic Swarm Verifier for Faulty systems), built on top of PSV-CA [Lomuscio and Pirovano, 2019], which in turn uses PRISM 4.0 [Kwiatkowska et al., 2011] as its underlying probabilistic model checker. |
| Experiment Setup | Yes | The protocol has agents in four possible states: resting in a nest, searching for food, reaching some food, and returning to the nest with food. Resting robots may decide with probability 0.5 to begin searching for food. Robots searching for food may find some with probability 0.3. After two time-steps of failed searching, the robot goes back to resting. If a robot locates food, it moves towards it, picks it up, brings it back to the nest, then goes back to resting. We inject one fault into the system encoding the fact that whenever a robot tries to move and is carrying food, it may drop the food with some probability pf. If it does this, it will return to the nest with no food. As in the original analysis we check the specification pattern P max p [F <kdeposited2], where deposited2 is an atomic proposition that holds if at least two units of food have been deposited in the nest and k is a parameter indicating the number of steps. Figure 2: For different fault probabilities pf and time-steps k, the maximum value of p for which P max p [F <kdeposited2] holds. |