Scalable Verification of Strategy Logic through Three-Valued Abstraction
Authors: Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga, Vadim Malvone, Aniello Murano
IJCAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results. and 6 Experiments |
| Researcher Affiliation | Academia | Francesco Belardinelli1 , Angelo Ferrando2 , Wojciech Jamroga3 , Vadim Malvone4 , Aniello Murano5 1Imperial College London, United Kingdom 2University of Genoa, Italy 3Sn T, University of Luxembourg & Institute of Computer Science, Polish Academy of Sciences 4Telecom Paris, France 5University of Naples Federico II, Italy |
| Pseudocode | No | The paper does not contain any explicitly labeled 'Pseudocode' or 'Algorithm' blocks, nor does it present structured steps in a code-like format. |
| Open Source Code | Yes | We implemented a prototype tool in Java4... 4https://github.com/Angelo Ferrando/3-valued SL |
| Open Datasets | Yes | The case study we experimented on consists in a scheduler... The full description of the example can be found in [Cerm ak et al., 2018]. |
| Dataset Splits | No | The paper focuses on model checking and does not involve traditional training, validation, or test dataset splits common in machine learning tasks. |
| Hardware Specification | Yes | We carried out the experiments on a machine with the following specifications: Intel(R) Core(TM) i7-7700HQ CPU @ 2.80GHz, 4 cores 8 threads, 16 GB RAM DDR4. |
| Software Dependencies | No | The paper states 'implemented a prototype tool in Java' and uses 'MCMAS', 'MCMAS extension for SL[1G]', and 'MCMAS extension for SLK' but does not provide specific version numbers for Java or MCMAS. |
| Experiment Setup | Yes | The case study we experimented on consists in a scheduler..., the abstraction is assumed to be guided by an expert of the system. In more detail, all states where at least one process is waiting to be selected by the scheduler are clustered together., and the specific formula φ = x, y(Arbiter, x)(P1, y1) . . . (Pn, yn) G Wn i=1 Wn j=i+1 rsi rsj. |