On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
Authors: Raven Beutner, Bernd Finkbeiner
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implement our model-checking algorithm in a tool we call Hy MASMC and evaluate it on a range of benchmarks. 6 Implementation and Experiments |
| Researcher Affiliation | Academia | Raven Beutner, Bernd Finkbeiner CISPA Helmholtz Center for Information Security, Germany |
| Pseudocode | Yes | Algorithm 1: Model-checking algorithm for Hyper ATL S. |
| Open Source Code | No | The paper states, 'We have implemented our algorithm in a tool we call Hy MASMC.' and mentions supplementary material in a CoRR paper, but does not provide a direct link or explicit statement about the open-sourcing of the Hy MASMC tool's code. |
| Open Datasets | Yes | We use the same benchmark family used by Cerm ak, Lomuscio, and Murano (2015)... and As underlying MAS models, we use the ISPL models used by MCMAS (Cerm ak, Lomuscio, and Raimondi 2009)... |
| Dataset Splits | No | The paper evaluates on 'benchmarks' and 'ISPL models' which are concurrent game structures, but it does not specify any train/validation/test dataset splits as these are not typically applicable in model checking verification. |
| Hardware Specification | Yes | All results were obtained on a 3.60GHz Xeon CPU (E31271) with 32GB of memory running Ubuntu 20.04. |
| Software Dependencies | No | The paper mentions using 'spot' and 'oink' libraries, stating: 'For automata operations (in particular, the translation from alternating to deterministic automata), we use spot; an actively-maintained automata library (Duret-Lutz et al. 2022). To check APAs over the singleton alphabet ( S) for emptiness, we use the parity-game solver oink (van Dijk 2018).' However, specific version numbers for these software dependencies are not provided. |
| Experiment Setup | Yes | For each ISPL model, we sample 20 random Hyper ATL S formulas from each of the templates and display the verification times in Table 2. Using Hy MASMC, we can, for the first first time, automatically check properties beyond the self-composition fragment of Hyper ATL the largest fragment supported by previous tools... We evaluate Hy MASMC by verifying a range of properties in MASs from the literature. |