A model checker for verifying ConGolog programs

Abstract

We describe our work in progress on a model checker for ver-ifying 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 cor-rectness. We apply the techniques from XSB tabling and the µ-calculus, to overcome the challenge of verifying complex non-terminating programs, in a terminating time. This note describes our work on a model checker (Clarke Jr., Grumberg, & Peled 1999) for verifying ConGolog pro-grams. ConGolog is a programming language for high-level control of robots (De Giacomo, Lespérance, & Levesque 2000). The language is based on the situation calculus, a for-