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

@INPROCEEDINGS{Classen2018,
author = {Jens Cla{\ss}en},
title = {Symbolic Verification of {G}olog Programs with
First-Order {BDD}s},
booktitle = {Proceedings of the Sixteenth International Conference
on Principles of Knowledge Representation and
Reasoning (KR 2018)},
pages = {524--528},
year = {2018},
editor = {Michael Thielscher and Francesca Toni and Frank Wolter},
publisher = {AAAI Press},
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.},
url = {https://kbsg.rwth-aachen.de/~classen/pub/Classen2018.pdf}
}

Downloads: 0

{"_id":"JcBuGPRHzk5mHJ9YT","bibbaseid":"claen-symbolicverificationofgologprogramswithfirstorderbdds-2018","author_short":["Claßen, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]}],"title":"Symbolic Verification of Golog Programs with First-Order BDDs","booktitle":"Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)","pages":"524–528","year":"2018","editor":[{"firstnames":["Michael"],"propositions":[],"lastnames":["Thielscher"],"suffixes":[]},{"firstnames":["Francesca"],"propositions":[],"lastnames":["Toni"],"suffixes":[]},{"firstnames":["Frank"],"propositions":[],"lastnames":["Wolter"],"suffixes":[]}],"publisher":"AAAI Press","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.","url":"https://kbsg.rwth-aachen.de/~classen/pub/Classen2018.pdf","bibtex":"@INPROCEEDINGS{Classen2018,\n author = {Jens Cla{\\ss}en},\n title = {Symbolic Verification of {G}olog Programs with\n First-Order {BDD}s},\n booktitle = {Proceedings of the Sixteenth International Conference\n on Principles of Knowledge Representation and\n Reasoning (KR 2018)},\n pages = {524--528},\n year = {2018},\n editor = {Michael Thielscher and Francesca Toni and Frank Wolter},\n publisher = {AAAI Press},\n abstract = {Golog is an agent language that allows defining\n behaviours in terms of programs over actions defined\n in a Situation Calculus action theory. Often it is\n vital to verify such a program against a temporal\n specification before deployment. So far work on the\n verification of Golog has been mostly of theoretical\n nature. Here we report on our efforts on\n implementing a verification algorithm for Golog\n based on fixpoint computations, a graph\n representation of program executions, and a symbolic\n representation of the state space. We describe the\n techniques used in our implementation, in particular\n a first-order variant of OBDDs for compactly\n representing formulas. We evaluate the approach by\n experimental analysis.},\n url = {https://kbsg.rwth-aachen.de/~classen/pub/Classen2018.pdf}\n}\n\n","author_short":["Claßen, J."],"editor_short":["Thielscher, M.","Toni, F.","Wolter, F."],"key":"Classen2018","id":"Classen2018","bibbaseid":"claen-symbolicverificationofgologprogramswithfirstorderbdds-2018","role":"author","urls":{"Paper":"https://kbsg.rwth-aachen.de/~classen/pub/Classen2018.pdf"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["symbolic","verification","golog","programs","first","order","bdds","claßen"],"title":"Symbolic Verification of Golog Programs with First-Order BDDs","year":2018}