@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}
}

{"_id":"s6T5Pg6Qw29hE9h4M","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":{}}},"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}