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.
The HYBRIS A1 project.
The action language GOLOG has been used, among other things, for the specification of the behaviour of mobile robots. Since the task of such autonomous systems is typically open-ended, their GOLOG programs are usually non-terminating. To ensure that the program will let the robot exhibit the intended behaviour, it is often desirable to be able to formally specify and then verify the desired properties, which are often of a temporal nature. This task has been studied within our preliminary work from two perspectives: On the one hand, the problem was tackled for very expressive specification and action program formalisms, but without the goal of achieving decidability, i.e. the developed verification methods were not guaranteed to terminate. On the other hand, the verification problem was studied for action formalisms based on decidable description logics and very limited means of specifying admissible sequences of actions, which allowed us to show decidability and complexity results for the verification problem. The purpose of this project is to combine the advantages of both approaches by, on one hand, developing verification methods for GOLOG programs that are effective and practically feasible and, on the other hand, going beyond the formalisms with very limited expressiveness to enhance their usefulness. Among other things, both qualitative and quantitative temporal program properties will be addressed.