On Decidable Verification of Non-terminating Golog Programs. Claßen, J., Liebenberg, M., & Lakemeyer, G. In Ji, J., Strass, H., & Wang, X., editors, Proceedings of the 10th International Workshop on Nonmonotonic Reasoning, Action and Change (NRAC 2013), pages 13–20, Beijing, China, 2013.
On Decidable Verification of Non-terminating Golog Programs [pdf]Paper  abstract   bibtex   
The high-level action programming language Golog has proven to be a useful means for the control of autonomous agents such as mobile robots. Usually, such agents perform open-ended tasks, and their control programs are hence non-terminating. Before deploying such a program to the robot, it is often desirable if not crucial to verify that it meets certain requirements, preferably by means of an automated method. For this purpose, 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\textquoterights high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this paper, 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.

Downloads: 0