Verifying ConGolog Programs on Bounded Situation Calculus Theories
Authors: Giuseppe De Giacomo, Yves Lespérance, Fabio Patrizi, Sebastian Sardina
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We show that verification of μ-calculus temporal properties against Con Golog programs over such bounded theories is decidable in general. In this paper, we show that this is indeed the case: verification of firstorder μ-calculus temporal properties against Con Golog programs over bounded action theories is decidable. To obtain this result we develop a new transition semantics for Con Golog programs, which is shown equivalent to the original one, that keeps bindings of nondeterministically picked object variables in a separate program environment whose size in terms of number of pick variables is naturally bounded. |
| Researcher Affiliation | Academia | Giuseppe De Giacomo Sapienza Univ. Roma Rome, Italy degiacomo@dis.uniroma1.it Yves Lesp erance York University Toronto, ON, Canada lesperan@cse.yorku.ca Fabio Patrizi Free Univ. Bozen/Bolzano Bolzano, Italy patrizi@inf.unibz.it Sebastian Sardina RMIT University Melbourne, Australia sebastian.sardina@rmit.edu.au |
| Pseudocode | Yes | Procedure 1 Construction of Fδ0,M. Qf := {q0}; qf 0 := q0; f:= ; Lf(q0) := L(q0); Qf F := ; if (q0 QF ) then Qf F := {q0}; repeat pick q = (δ, x, s) Qf; for all (q = (δ , x , s ) | q q in Tδ0,M) if ( q = (δ , x , s ) Qf | L(q ) Lf(q )) then f:= f { q, q }; else {Qf := Qf {q }; Lf(q ) := L(q ); f:= f { q, q } } if (q QF ) then Qf F := Qf F {q } until (transition relation f does not change any more) |
| Open Source Code | No | The paper does not provide any statement or link indicating that source code for the described methodology is publicly available. |
| Open Datasets | No | The paper does not mention the use of any datasets, public or otherwise. It is a theoretical paper focusing on decidability. |
| Dataset Splits | No | The paper does not describe experiments that would involve training, validation, or test dataset splits. |
| Hardware Specification | No | The paper does not provide any specific hardware details used for running experiments, as it is a theoretical paper. |
| Software Dependencies | No | The paper does not mention any specific software dependencies with version numbers, as it is a theoretical work. |
| Experiment Setup | No | The paper does not describe any experimental setup details, hyperparameters, or training configurations. |