Symbolic Verification of Golog Programs with First-Order BDDs. Claßen, J. 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.
Symbolic Verification of Golog Programs with First-Order BDDs [pdf]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.

Downloads: 0