Automatic Verification of Liveness Properties in the Situation Calculus
Authors: Jian Li, Yongmei Liu2886-2892
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented the proposed method and experimented with the blocks world domain and a number of other domains from the literature. Experimental results showed that most goals can be verified within a reasonable amount of time. [...] We implemented a verification system based on the proposed method and conducted a set of experiments on it. Experimental results showed that most goals can be verified within a reasonable amount of time. [...] Table 1 shows our experimental results for blocks world. |
| Researcher Affiliation | Academia | Jian Li, Yongmei Liu Dept. of Computer Science, Sun Yat-sen University, Guangzhou 510006, China lijian77@mail3.sysu.edu.cn, ymliu@mail.sysu.edu.cn |
| Pseudocode | Yes | The paper includes several algorithms labeled as such: 'Algorithm 1: diverify(D, ϕ)', 'Algorithm 2: verify(D, ϕ)', 'Algorithm 3: induction(D, ϕ, f)', and 'Algorithm 4: gen Features(D, ϕ)'. |
| Open Source Code | No | The paper states, 'We implemented our verification method in python3 using the FF planner (Hoffmann and Nebel 2001) and the SMT solver Z3 (de Moura and Bjørner 2008).', but it does not provide a link or explicit statement about releasing the source code for their implementation. |
| Open Datasets | No | The paper defines axioms for standard AI planning domains like 'blocks world', 'Oil lamp', 'Chop tree', 'Pick up Stone', and 'Corner'. It also mentions generating 'small models' using SMT solvers for these domains to create planning problems. However, it does not refer to or provide access to a pre-existing, fixed, publicly available 'dataset' in the conventional sense (e.g., with a link, DOI, or formal citation). |
| Dataset Splits | No | The paper does not mention specific training, validation, or test dataset splits. It describes generating small models for planning problems, which does not involve traditional data splitting. |
| Hardware Specification | Yes | All experiments were run on a Linux machine with 2.40GHz CPU and 16GB RAM. |
| Software Dependencies | No | The paper mentions 'python3', 'FF planner (Hoffmann and Nebel 2001)', and 'SMT solver Z3 (de Moura and Bjørner 2008)', but it does not specify exact version numbers for these software components, which is required for a reproducible description. |
| Experiment Setup | Yes | We set up the implementation parameters as follows: The time-out bound for Z3 is 5 seconds; when generating potential features, the bound of feature size is 2, the number of planning problems is 3, λ1 = 0.8 and λ2 = 1.0; the k in k is set to 2. |