A Model Checker for Verifying ConGolog Programs

Leila Kalantari and Eugenia Ternovska, Simon Fraser University

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 correctness. 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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.