Diploma Thesis: Towards Decidable Verification of Non-Terminating Golog Programs [completed]

Submitted by Martin Liebenberg on 13. April 2013 - 20:45

Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of non-terminating Golog programs, based on the first-order modal Situation Calculus variant ES, and regression-based reasoning. However, while Golog’s high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this thesis, we address this problem by showing that, for a relevant subset, the verification of non-terminating Golog programs is indeed decidable, which is achieved by means of three restrictions. First, we use the ES variant of a decidable two-variable fragment of the Situation Calculus that was introduced by Gu and Soutchanski. Second, we have to restrict the Golog program to contain ground action only. Finally, we consider special classes of successor state axioms, namely the context-free ones and those that only admit local effects.