@INPROCEEDINGS{ZarriessClassen2016a,
  author      = {Benjamin Zarrie{\ss} and Jens Cla{\ss}en},
  title       = {Decidable Verification of {G}olog Programs over
                  Non-Local Effect Actions},
  booktitle   = {Proceedings of the Thirtieth AAAI Conference on
                  Artificial Intelligence (AAAI 2016)},
  year        = {2016},
  pages       = {1109--1115},
  publisher   = {AAAI Press},
  editor      = {Dale Schuurmans and Michael Wellman},
  abstract    = {The Golog action programming language is a powerful
                  means to express high-level behaviours in terms of
                  programs over actions defined in a Situation
                  Calculus theory. In particular for physical systems,
                  verifying that the program satisfies certain desired
                  temporal properties is often crucial, but
                  undecidable in general, the latter being due to the
                  language{\textquoteright}s high expressiveness in
                  terms of first-order quantification, range of action
                  effects, and program constructs. So far, approaches
                  to achieve decidability involved restrictions where
                  action effects either had to be context-free
                  (i.e. not depend on the current state), local
                  (i.e. only affect objects mentioned in the
                  action{\textquoteright}s parameters), or at least
                  bounded (i.e. only affect a finite number of
                  objects). In this paper, we introduce two new, more
                  general classes of action theories that allow for
                  context-sensitive, non-local, unbounded effects,
                  i.e. actions that may affect an unbounded number of
                  possibly unnamed objects in a state-dependent
                  fashion. We contribute to the further exploration of
                  the boundary between decidability and undecidability
                  for Golog, showing that for our new classes of
                  action theories in the two-variable fragment of
                  first-order logic, verification of CTL* properties
                  of programs over ground actions is decidable.},
  url         = {https://kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2016a.pdf}
}

{"_id":"pBzffbbf44zZf57iN","bibbaseid":"zarrie-claen-decidableverificationofgologprogramsovernonlocaleffectactions-2016","author_short":["Zarrieß, B.","Claßen, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Benjamin"],"propositions":[],"lastnames":["Zarrieß"],"suffixes":[]},{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]}],"title":"Decidable Verification of Golog Programs over Non-Local Effect Actions","booktitle":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI 2016)","year":"2016","pages":"1109–1115","publisher":"AAAI Press","editor":[{"firstnames":["Dale"],"propositions":[],"lastnames":["Schuurmans"],"suffixes":[]},{"firstnames":["Michael"],"propositions":[],"lastnames":["Wellman"],"suffixes":[]}],"abstract":"The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language\\textquoterights high expressiveness in terms of first-order quantification, range of action effects, and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be context-free (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action\\textquoterights parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we introduce two new, more general classes of action theories that allow for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for our new classes of action theories in the two-variable fragment of first-order logic, verification of CTL* properties of programs over ground actions is decidable.","url":"https://kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2016a.pdf","bibtex":"@INPROCEEDINGS{ZarriessClassen2016a,\n author = {Benjamin Zarrie{\\ss} and Jens Cla{\\ss}en},\n title = {Decidable Verification of {G}olog Programs over\n Non-Local Effect Actions},\n booktitle = {Proceedings of the Thirtieth AAAI Conference on\n Artificial Intelligence (AAAI 2016)},\n year = {2016},\n pages = {1109--1115},\n publisher = {AAAI Press},\n editor = {Dale Schuurmans and Michael Wellman},\n abstract = {The Golog action programming language is a powerful\n means to express high-level behaviours in terms of\n programs over actions defined in a Situation\n Calculus theory. In particular for physical systems,\n verifying that the program satisfies certain desired\n temporal properties is often crucial, but\n undecidable in general, the latter being due to the\n language{\\textquoteright}s high expressiveness in\n terms of first-order quantification, range of action\n effects, and program constructs. So far, approaches\n to achieve decidability involved restrictions where\n action effects either had to be context-free\n (i.e. not depend on the current state), local\n (i.e. only affect objects mentioned in the\n action{\\textquoteright}s parameters), or at least\n bounded (i.e. only affect a finite number of\n objects). In this paper, we introduce two new, more\n general classes of action theories that allow for\n context-sensitive, non-local, unbounded effects,\n i.e. actions that may affect an unbounded number of\n possibly unnamed objects in a state-dependent\n fashion. We contribute to the further exploration of\n the boundary between decidability and undecidability\n for Golog, showing that for our new classes of\n action theories in the two-variable fragment of\n first-order logic, verification of CTL* properties\n of programs over ground actions is decidable.},\n url = {https://kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2016a.pdf}\n}\n\n","author_short":["Zarrieß, B.","Claßen, J."],"editor_short":["Schuurmans, D.","Wellman, M."],"key":"ZarriessClassen2016a","id":"ZarriessClassen2016a","bibbaseid":"zarrie-claen-decidableverificationofgologprogramsovernonlocaleffectactions-2016","role":"author","urls":{"Paper":"https://kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2016a.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["decidable","verification","golog","programs","over","non","local","effect","actions","zarrieß","claßen"],"title":"Decidable Verification of Golog Programs over Non-Local Effect Actions","year":2016}