@INPROCEEDINGS{ZarriessClassen2014b,
  author      = {Benjamin Zarrie{\ss} and Jens Cla{\ss}en},
  title       = {Verifying {CTL*} Properties of {G}olog Programs over
                  Local-Effect Actions},
  booktitle   = {Proceedings of the Twenty-First European Conference
                  on Artificial Intelligence (ECAI 2014)},
  year        = {2014},
  pages       = {939-944},
  publisher   = {IOS Press},
  abstract    = {Golog is a high-level action programming language for
                  controlling autonomous agents such as mobile
                  robots. It is defined on top of a logic-based action
                  theory expressed in the Situation Calculus. Before a
                  program is deployed onto an actual robot and
                  executed in the physical world, it is desirable, if
                  not crucial, to verify that it meets certain
                  requirements (typically expressed through temporal
                  formulas) and thus indeed exhibits the desired
                  behaviour. However, due to the high (first-order)
                  expressiveness of the language, the corresponding
                  verification problem is in general undecidable. In
                  this paper, we extend earlier results to identify a
                  large, non-trivial fragment of the formalism where
                  verification is decidable. In particular, we
                  consider properties expressed in a first-order
                  variant of the branching-time temporal logic
                  CTL*. Decidability is obtained by (1) resorting to
                  the decidable first-order fragment
                  C{\texttwosuperior} as underlying base logic, (2)
                  using a fragment of Golog with ground actions only,
                  and (3) requiring the action theory to only admit
                  local effects.},
  url         = {http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014b.pdf}
}

{"_id":"SZwM4FYrDd43x2PaX","bibbaseid":"zarrie-claen-verifyingctlpropertiesofgologprogramsoverlocaleffectactions-2014","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":"Verifying CTL* Properties of Golog Programs over Local-Effect Actions","booktitle":"Proceedings of the Twenty-First European Conference on Artificial Intelligence (ECAI 2014)","year":"2014","pages":"939-944","publisher":"IOS Press","abstract":"Golog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL*. Decidability is obtained by (1) resorting to the decidable first-order fragment C\\texttwosuperior as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects.","url":"http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014b.pdf","bibtex":"@INPROCEEDINGS{ZarriessClassen2014b,\n author = {Benjamin Zarrie{\\ss} and Jens Cla{\\ss}en},\n title = {Verifying {CTL*} Properties of {G}olog Programs over\n Local-Effect Actions},\n booktitle = {Proceedings of the Twenty-First European Conference\n on Artificial Intelligence (ECAI 2014)},\n year = {2014},\n pages = {939-944},\n publisher = {IOS Press},\n abstract = {Golog is a high-level action programming language for\n controlling autonomous agents such as mobile\n robots. It is defined on top of a logic-based action\n theory expressed in the Situation Calculus. Before a\n program is deployed onto an actual robot and\n executed in the physical world, it is desirable, if\n not crucial, to verify that it meets certain\n requirements (typically expressed through temporal\n formulas) and thus indeed exhibits the desired\n behaviour. However, due to the high (first-order)\n expressiveness of the language, the corresponding\n verification problem is in general undecidable. In\n this paper, we extend earlier results to identify a\n large, non-trivial fragment of the formalism where\n verification is decidable. In particular, we\n consider properties expressed in a first-order\n variant of the branching-time temporal logic\n CTL*. Decidability is obtained by (1) resorting to\n the decidable first-order fragment\n C{\\texttwosuperior} as underlying base logic, (2)\n using a fragment of Golog with ground actions only,\n and (3) requiring the action theory to only admit\n local effects.},\n url = {http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014b.pdf}\n}\n\n","author_short":["Zarrieß, B.","Claßen, J."],"key":"ZarriessClassen2014b","id":"ZarriessClassen2014b","bibbaseid":"zarrie-claen-verifyingctlpropertiesofgologprogramsoverlocaleffectactions-2014","role":"author","urls":{"Paper":"http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014b.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["verifying","ctl","properties","golog","programs","over","local","effect","actions","zarrieß","claßen"],"title":"Verifying CTL* Properties of Golog Programs over Local-Effect Actions","year":2014}