Reachability Games Modulo Theories with a Bounded Safety Player
Authors: Marco Faella, Gennaro Parlato
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We demonstrate that GMTs can model various relevant real-world games, and that our approach can effectively solve several problems from different domains, using Z3 as the backend CHC solver. and Experiments We now report a selection of experiments comparing our approach to the state-of-the-art. |
| Researcher Affiliation | Academia | Marco Faella1, Gennaro Parlato2 1 University of Naples Federico II, Naples, Italy 2 University of Molise, Pesche, Italy |
| Pseudocode | Yes | Algorithm 1: Synthesizing a winning strategy for REACH if a counterexample is available. and similar for Algorithm 2 and 3. |
| Open Source Code | No | The paper mentions using Z3 as a backend CHC solver, but it does not provide a link or explicit statement about the availability of its own source code for the methodology described. |
| Open Datasets | No | The paper applies its method to problem settings such as the "Cinderella-Stepmother game", a "program synthesis example" from Beyene et al. (2014) and Farzan and Kincaid (2018), and "Nim". These are problem descriptions or benchmarks, not traditional datasets for which public access links or formal citations (beyond the original problem paper) are provided. |
| Dataset Splits | No | The paper deals with reachability games and their configurations, which are not typically partitioned into training, validation, and test sets like datasets in machine learning. There is no mention of dataset split percentages or methodologies. |
| Hardware Specification | Yes | All experiments were performed on the virtual machine provided by Baier et al. (2021), running on an AMD Ryzen 2700X with 16GB of RAM. The VM was allotted 4 CPUs and 6GB of RAM. |
| Software Dependencies | Yes | The CHC solver was Z3 v.4.8.7 64bit (de Moura and Bjørner 2008), whose CHC engine is based on SPACER (Komuravelli et al. 2013). |
| Experiment Setup | Yes | The experiment consisted in designing a system of CHCs in the shape of Figure 1 in the language SMT-LIB and feeding it to the SMT-solver Z3 (see (de Moura and Bjørner 2008)). |