Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models
Authors: Damian Kurpiewski, Wojciech Jamroga, Yan Kim
IJCAI 2025 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We conducted two sets of experiments to evaluate the performance of our approach. The first set focused on the standard Asynchronous Simple Voting model, while the second set examined the same model with the addition of revoting. In the experiments, we compared the verification time of fixpoint approximation on local approximation models vs. the performance of the fixpoint approximation on standard global model, implemented in the state-of-art model checker STV [Kurpiewski et al., 2024], that operates on explicit representation of global states. The results (discussed further) show astonishing gains. One may notice, however, that in order to run the approximate verification, we should first generate the local approximating model. |
| Researcher Affiliation | Academia | 1Institute of Computer Science, Polish Academy of Sciences 2Nicolaus Copernicus University in Toru n, Poland 3Interdisciplinary Centre for Security, Reliability, and Trust, Sn T, University of Luxembourg |
| Pseudocode | No | The paper describes algorithms and logical formalisms through definitions and proofs, but does not include any clearly labeled pseudocode blocks, figures, or structured algorithm sections. For example, Definition 13 details 'Lower Approximation for s ATL ir' using logical formulas rather than pseudocode. |
| Open Source Code | Yes | The code for the experiments is available at https://tinyurl.com/sup7888. |
| Open Datasets | No | The paper focuses on model checking and uses 'scalable models of voting' (e.g., ASVk n) as its experimental subject, which are formally defined systems rather than traditional datasets. It does not provide access to a specific, pre-existing publicly available dataset in the conventional sense (e.g., image datasets, text corpora) with a link or citation. |
| Dataset Splits | No | The paper deals with model checking formal systems (scalable models of voting) rather than empirical datasets, so the concept of training/test/validation splits does not apply. The experiments are conducted on generated models, and no dataset splits are relevant or mentioned. |
| Hardware Specification | Yes | All experiments were conducted on a machine equipped with a 3.0 GHz 8-core AMD Ryzen 7 5700X3D CPU and 64 GB of RAM. |
| Software Dependencies | No | The paper mentions using the 'state-of-art model checker STV [Kurpiewski et al., 2024]' and the 'UPPAAL model checker [Behrmann et al., 2004]'. While specific tools are named, explicit version numbers for these software components, beyond their citation years, are not provided in the text. |
| Experiment Setup | Yes | The verified formula was ϕ1 = V oter1 F (vote1,1 give1). The approximated model was generated for agent V oter1. In all scenarios, there were two candidates and one coercer. All experiments were conducted on a machine equipped with a 3.0 GHz 8-core AMD Ryzen 7 5700X3D CPU and 64 GB of RAM. All times are reported in seconds, with a timeout set to two hours. |