AAAI Publications, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning

Font Size: 
Symbolic Verification of Golog Programs with First-Order BDDs
Jens Classen

Last modified: 2018-09-24


Golog is an agent language that allows defining behaviours in terms of programs over actions defined in a Situation Calculus action theory. Often it is vital to verify such a program against a temporal specification before deployment. So far work on the verification of Golog has been mostly of theoretical nature. Here we report on our efforts on implementing a verification algorithm for Golog based on fixpoint computations, a graph representation of program executions, and a symbolic representation of the state space. We describe the techniques used in our implementation, in particular a first-order variant of OBDDs for compactly representing formulas. We evaluate the approach by experimental analysis.


Situation Calculus; Golog; Verification; OBDD

Full Text: PDF