@INPROCEEDINGS{LiebenbergAAAI14,
  author      = {Jens Cla{\ss}en and Martin Liebenberg and Gerhard
                  Lakemeyer and Benjamin Zarrie{\ss}},
  title       = {Exploring the Boundaries of Decidable Verification of
                  Non-Terminating {G}olog Programs},
  booktitle   = {Proceedings of the Twenty-Eighth AAAI Conference on
                  Artificial Intelligence (AAAI 2014)},
  year        = {2014},
  address     = {Québec, Canada},
  pages       = {1012--1019},
  publisher   = {AAAI Press},
  abstract    = {The action programming language Golog has been found
                  useful for the control of autonomous agents such as
                  mobile robots. In scenarios like these, tasks are
                  often open-ended so that the respective control
                  programs are non-terminating. Before deploying such
                  programs on a robot, it is often desirable to verify
                  that they meet certain requirements. For this
                  purpose, Cla{\ss}en and Lakemeyer recently
                  introduced algorithms for the verification of
                  temporal properties of Golog programs. However,
                  given the expressiveness of Golog, their
                  verification procedures are not guaranteed to
                  terminate. In this paper, we show how decidability
                  can be obtained by suitably restricting the
                  underlying base logic, the effect axioms for
                  primitive actions, and the use of actions within
                  Golog programs. Moreover, we show that dropping any
                  of these restrictions immediately leads to
                  undecidability of the verification problem.},
  url         = {http://www.kbsg.rwth-aachen.de/~classen/pub/ClassenEtAl2014.pdf}
}

{"_id":"mkj3Zi2QhxC3k9XzY","bibbaseid":"claen-liebenberg-lakemeyer-zarrie-exploringtheboundariesofdecidableverificationofnonterminatinggologprograms-2014","author_short":["Claßen, J.","Liebenberg, M.","Lakemeyer, G.","Zarrieß, B."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]},{"firstnames":["Martin"],"propositions":[],"lastnames":["Liebenberg"],"suffixes":[]},{"firstnames":["Gerhard"],"propositions":[],"lastnames":["Lakemeyer"],"suffixes":[]},{"firstnames":["Benjamin"],"propositions":[],"lastnames":["Zarrieß"],"suffixes":[]}],"title":"Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs","booktitle":"Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI 2014)","year":"2014","address":"Québec, Canada","pages":"1012–1019","publisher":"AAAI Press","abstract":"The action programming language Golog has been found useful for the control of autonomous agents such as mobile robots. In scenarios like these, tasks are often open-ended so that the respective control programs are non-terminating. Before deploying such programs on a robot, it is often desirable to verify that they meet certain requirements. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of Golog programs. However, given the expressiveness of Golog, their verification procedures are not guaranteed to terminate. In this paper, we show how decidability can be obtained by suitably restricting the underlying base logic, the effect axioms for primitive actions, and the use of actions within Golog programs. Moreover, we show that dropping any of these restrictions immediately leads to undecidability of the verification problem.","url":"http://www.kbsg.rwth-aachen.de/~classen/pub/ClassenEtAl2014.pdf","bibtex":"@INPROCEEDINGS{LiebenbergAAAI14,\n author = {Jens Cla{\\ss}en and Martin Liebenberg and Gerhard\n Lakemeyer and Benjamin Zarrie{\\ss}},\n title = {Exploring the Boundaries of Decidable Verification of\n Non-Terminating {G}olog Programs},\n booktitle = {Proceedings of the Twenty-Eighth AAAI Conference on\n Artificial Intelligence (AAAI 2014)},\n year = {2014},\n address = {Québec, Canada},\n pages = {1012--1019},\n publisher = {AAAI Press},\n abstract = {The action programming language Golog has been found\n useful for the control of autonomous agents such as\n mobile robots. In scenarios like these, tasks are\n often open-ended so that the respective control\n programs are non-terminating. Before deploying such\n programs on a robot, it is often desirable to verify\n that they meet certain requirements. For this\n purpose, Cla{\\ss}en and Lakemeyer recently\n introduced algorithms for the verification of\n temporal properties of Golog programs. However,\n given the expressiveness of Golog, their\n verification procedures are not guaranteed to\n terminate. In this paper, we show how decidability\n can be obtained by suitably restricting the\n underlying base logic, the effect axioms for\n primitive actions, and the use of actions within\n Golog programs. Moreover, we show that dropping any\n of these restrictions immediately leads to\n undecidability of the verification problem.},\n url = {http://www.kbsg.rwth-aachen.de/~classen/pub/ClassenEtAl2014.pdf}\n}\n\n\n","author_short":["Claßen, J.","Liebenberg, M.","Lakemeyer, G.","Zarrieß, B."],"key":"LiebenbergAAAI14","id":"LiebenbergAAAI14","bibbaseid":"claen-liebenberg-lakemeyer-zarrie-exploringtheboundariesofdecidableverificationofnonterminatinggologprograms-2014","role":"author","urls":{"Paper":"http://www.kbsg.rwth-aachen.de/~classen/pub/ClassenEtAl2014.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["exploring","boundaries","decidable","verification","non","terminating","golog","programs","claßen","liebenberg","lakemeyer","zarrieß"],"title":"Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs","year":2014}