Automatic Verification of Partial Correctness of Golog Programs

When Golog programs are used to control agents' behaviour in a high-level manner, their partial correctness naturally becomes an important concern. In this paper we propose a sound but incomplete method for automatic verification of partial correctness of Golog programs. We introduce the notion of extended regression, which reduces partial correctness of Golog programs to first-order entailment problems. During the process loop invariants are automatically discovered by heuristic methods. We propose progression of small models wrt Golog programs, which are used to filter out too strong heuristic candidates. In this way we combine the methods of static and dynamic analysis from the software engineering community. Furthermore, our method can also be adapted to verify state constraints. Experiments show that our method can not only handle sequential and nested loops uniformly in a reasonable among of time, but also be used to discover succinct and comprehensible loop invariants and state constraints.