Automated Synthesis of Generalized Invariant Strategies via Counterexample-Guided Strategy Refinement
Authors: Kailun Luo, Yongmei Liu5800-5808
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented our method and did experiments with a number of game problems. Our system can successfully synthesize solutions for most of the domains within a reasonable amount of time. |
| Researcher Affiliation | Academia | Kailun Luo,1,2 Yongmei Liu2 1 School of Cyberspace Security, Dongguan University of Technology, Dongguan 523808, China 2 Dept. of Computer Science, Sun Yat-sen University, Guangzhou 510006, China |
| Pseudocode | Yes | Algorithm 1: synthesize; Algorithm 2: refine; Algorithm 3: find Safe Region |
| Open Source Code | No | The paper states 'We implemented a prototype system using Python.' but does not provide any statement or link about the availability of the source code. |
| Open Datasets | No | The paper describes how game instances are generated from an 'initial database' and by using an SMT solver with a bound, but it does not use or provide access to a publicly available or open dataset in the traditional sense. |
| Dataset Splits | No | The paper does not specify any training, validation, or test dataset splits. |
| Hardware Specification | Yes | All experiments were conducted on a Mac OS machine with 2.30GHz CPU and 8GB RAM. |
| Software Dependencies | No | We use two SMT solvers for the first-order reasoning: Z3 [de Moura and Bjørner 2008] and CVC4 [Barrett et al. 2011]... We use the multi-agent model checker MCMAS [Lomuscio, Qu, and Raimondi 2017]... The paper lists software names but does not specify version numbers for Z3, CVC4, or MCMAS. |
| Experiment Setup | Yes | Considering the computational resources, we set the number c in Alg. 3 to 1, and the number k in Alg. 2 to 3. The time-out bound for the main algorithm is 3600 seconds. The time-out bound for the SMT solvers is 10 seconds. |