Decidable Verification of Golog Programs over Non-Local Effect Actions

Authors: Benjamin Zarrieß, Jens Claßen

AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for our new classes of action theories in the two-variable fragment of first-order logic, verification of CTL properties of programs over ground actions is decidable.
Researcher Affiliation Academia Benjamin Zarrieß Theoretical Computer Science TU Dresden, Germany benjamin.zarriess@tu-dresden.de Jens Claßen Knowledge-Based Systems Group RWTH Aachen University, Germany classen@kbsg.rwth-aachen.de
Pseudocode No The paper does not contain any explicit pseudocode blocks or algorithms labeled as such. It presents definitions and mathematical formulations.
Open Source Code No The paper does not provide any statements about making source code for their methodology openly available, nor does it include a link to a code repository.
Open Datasets No The paper is theoretical and does not use or reference any datasets for training. Examples provided are illustrative, not empirical data.
Dataset Splits No The paper is theoretical and does not involve empirical validation with dataset splits (training, validation, or test). Therefore, no such information is provided.
Hardware Specification No The paper is theoretical and does not describe any experiments that would require specific hardware. No hardware specifications are mentioned.
Software Dependencies No The paper describes theoretical frameworks (e.g., Situation Calculus, C2, ES logic) but does not mention any specific software dependencies with version numbers required for replication of empirical work, as no experiments are conducted.
Experiment Setup No The paper is theoretical and does not describe any experimental setup details, hyperparameters, or training configurations, as no empirical experiments are conducted.