Content: Publications

Symbolic Verification of Golog Programs with First-Order BDDs

In Proc. Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), pp. 524--528

Authors:Jens Claßen
Type:Article in Conference Proceedings
Publication Date:October 2018
Download:Classen2018.pdf
Conference:Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)
Editor:Michael Thielscher, Francesca Toni, Frank Wolter

Abstract: 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.

BibTeX
@InProceedings{hybris-a1-evaluation_BDD-2018,
  title =	{{Symbolic Verification of Golog Programs with First-Order BDDs}},
  author =	{Jens Claßen},
  booktitle =	{Proc. of Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)},
  year =	{2018},
  editor =	{Michael Thielscher, Francesca Toni, Frank Wolter},
  publisher =	{AAAI Press},
  pages =	{524--528},
}