Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs
Authors: Jens Classen, Martin Liebenberg, Gerhard Lakemeyer, Benjamin Zarriess
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we show how decidability can be obtained by suitably restricting the underlying base logic, the effect axioms for primitive actions, and the use of actions within GOLOG programs. Moreover, we show that dropping any of these restrictions immediately leads to undecidability of the verification problem. |
| Researcher Affiliation | Academia | Jens Claßen, Martin Liebenberg and Gerhard Lakemeyer Knowledge-Based Systems Group RWTH Aachen University, Germany {classen,liebenberg,gerhard}@kbsg.rwth-aachen.de Benjamin Zarrieß Theoretical Computer Science TU Dresden, Germany zarriess@tcs.inf.tu-dresden.de |
| Pseudocode | Yes | Procedure 1 CHECKEG[δ, φ] 1: L := LABEL[Gδ, ]; L := LABEL[Gδ, φ]; 2: while L L do 3: L := L; L := L AND PRE[Gδ, L ]; 4: end while 5: return INITLABEL[Gδ, L] |
| Open Source Code | No | In the future, we plan to further investigate the computational complexity of decidable verification and provide an implementation. |
| Open Datasets | No | No datasets were used as this is a theoretical paper focusing on decidability of verification. |
| Dataset Splits | No | No empirical experiments were conducted, thus no validation splits are provided. |
| Hardware Specification | No | No experimental hardware details are provided as this is a theoretical paper focusing on formal verification properties. |
| Software Dependencies | No | The paper mentions 'Nu SMV (Cimatti et al. 2002)' as a tool that might be used in future work, but no specific software dependencies with version numbers are listed for the work presented in this paper. |
| Experiment Setup | No | No empirical experiments were conducted, thus no experimental setup details like hyperparameters or training configurations are provided. |