Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems
Authors: Alessio Lomuscio, Edoardo Pirovano
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present an implementation and evaluate its performance on an ant coverage algorithm. |
| Researcher Affiliation | Academia | Alessio Lomuscio, Edoardo Pirovano Department of Computing Imperial College London, UK {a.lomuscio,e.pirovano17}@imperial.ac.uk |
| Pseudocode | Yes | Algorithm 1 EPI Decision Procedure; Algorithm 2 ETI Decision Procedure |
| Open Source Code | Yes | The sources and the models (including the one we evaluate below) are released as open source [PSVBD, 2018]. [PSV-BD, 2018] PSV-BD. Probabilistic Swarm Veriļ¬er for Bounde D time properties http://vas.doc.ic.ac. uk/software/psv-bd/, 2018. |
| Open Datasets | No | The paper describes modeling an ant coverage algorithm on an n x n grid. It does not use or provide access information for a publicly available or open dataset for training, but rather defines its simulation environment. |
| Dataset Splits | No | The paper describes a simulation environment and verification process, not a machine learning experiment that would involve splitting datasets into training, validation, or test sets. |
| Hardware Specification | Yes | running the tool with Open JDK 1.8 (64-bit version, 4GB heap size) on a machine running Ubuntu 17.10 (Linux kernel 4.13.0-38) and an Intel i7-6700 processor. |
| Software Dependencies | Yes | Open JDK 1.8 (64-bit version, 4GB heap size) on a machine running Ubuntu 17.10 (Linux kernel 4.13.0-38); built on top of PRISM 4.0 [Kwiatkowska et al., 2011] |
| Experiment Setup | Yes | For different values of n and p we first establish, by calling EPI on P p[F k all Visited] for increasing values of k, the least value for which this specification is an emergent property. Then, we call ETI on the corresponding specification to compute the emergence threshold for this. Table 1 shows the results obtained by running the tool with Open JDK 1.8 (64-bit version, 4GB heap size) on a machine running Ubuntu 17.10 (Linux kernel 4.13.0-38) and an Intel i7-6700 processor. |