In Thielscher, M., Toni, F., & Wolter, F., editors, Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), pages 524–528, 2018. AAAI Press. Paper abstract bibtex
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.