Jens Classen, Gerhard Lakemeyer
Typical Golog programs for robot control are non-terminating. Analyzing such programs so far requires meta-theoretic arguments involving complex fix-point constructions. In this paper we propose a logic based on the situation calculus variant ES, which includes elements from branching time, dynamic and process logics and where the meaning of programs is modelled as possibly infinite sequences of actions. We show how properties of non-terminating programs can be formulated in the logic and, for a subset of it, how existing ideas from symbolic model checking in temporal logic can be applied to automatically verify program properties.
Subjects: 11. Knowledge Representation; 3.6 Temporal Reasoning
Submitted: Jun 16, 2008