Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants
Authors: Kailun Luo, Yongmei Liu
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented our method and did experiments on combinatorial game and also single-agent domains. Experimental results showed that our system can successfully verify most of them within a reasonable amount of time. |
| Researcher Affiliation | Academia | Dept. of Computer Science, Sun Yat-sen University, Guangzhou 510006, China |
| Pseudocode | Yes | Algorithm 1: verify(D, S, p) |
| Open Source Code | No | The paper states 'We implemented our algorithm using Python and Z3' but provides no link or explicit statement about open-sourcing the code for the described methodology. |
| Open Datasets | No | The paper mentions using domains from 'combinatorial game literature' and 'generalized planning literature' (e.g., Chomp, Pick Stone), but does not provide specific access information (links, DOIs, or formal citations) for any datasets used. |
| Dataset Splits | No | The paper focuses on verifying game strategies and does not describe training, validation, or test dataset splits in the context of machine learning model training. |
| Hardware Specification | Yes | All experiments were conducted on a Linux machine with 3.50GHz CPU and 16GB RAM. |
| Software Dependencies | No | The paper states 'We implemented our algorithm using Python and Z3' but does not specify version numbers for either software component. |
| Experiment Setup | Yes | We set the implementation parameters as follows: The time-out bound for Z3 is 10 second; when updating the X-label, we use 2-neighbors of clauses; when generating predicates we use at most 2 variables and when generating clauses we use at most 4 variables. |