Abstract:
We describe our work in progress on a model checker for verifying ConGolog programs. ConGolog is a novel high-level programming language for robot control which incorporates a rich account of concurrency, prioritized execution, interrupts, and changes in the world that are beyond robot's control. The novelty of this language requires new methods of proving program correctness. Our proposal is based on a repetition property which implies that it is sufficient to check a property in an initial finite subtree of the infinite execution tree determined by a program. Having proved this property, we apply the techniques from XSB tabling and the $\mu$-calculus, to overcome the challenge of verifying complex non-terminating programs, in a terminating time.