A logic for non-terminating Golog programs

Abstract

Typical Golog programs for robot control are non-terminating. Analyzing such programs so far requires meta-theoretic arguments involving complex fix-point construc-tions. In this paper we propose a logic based on the situation calculus variant ES, which includes elements from branch-ing time, dynamic and process logics and where the meaning of programs is modelled as possibly infinite sequences of ac-tions. We show how properties of non-terminating programs can be formulated in the logic and, for a subset of it, how ex-isting ideas from symbolic model checking in temporal logic can be applied to automatically verify program properties.