@INPROCEEDINGS{ZarriessClassen2014a,
  author      = {Benjamin Zarrie{\ss} and Jens Cla{\ss}en},
  title       = {On the Decidability of Verifying {LTL} Properties of
                  {G}olog Programs},
  booktitle   = {Proceedings of the AAAI 2014 Spring Symposium:
                  Knowledge Representation and Reasoning in Robotics
                  (KRR'14)},
  year        = {2014},
  publisher   = {AAAI Press},
  abstract    = {The high-level action programming language Golog is a
                  useful means for modeling the behavior of autonomous
                  agents such as mobile robots. It relies on a
                  representation given in terms of a logic-based
                  action theory in the Situation Calculus (SC). To
                  guarantee that the possibly non-terminating
                  execution of a Golog program leads to the desired
                  behavior of the agent, it is desirable to
                  (automatically) verify that it satisfies certain
                  requirements given in terms of temporal
                  formulas. However, due to the high (first-order)
                  expressiveness of the Golog language, the
                  verification problem is in general undecidable. In
                  this paper we show that for a fragment of the Golog
                  language defined on top of the decidable logic
                  C{\texttwosuperior}, the verification problem for
                  linear time temporal properties becomes decidable,
                  which extends earlier results to a more expressive
                  fragment of the input formalism. Moreover, we
                  justify the involved restrictions on program
                  constructs and action theory by showing that
                  relaxing any of these restrictions instantly renders
                  the verification problem undecidable again.},
  url         = {http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014a.pdf}
}

{"_id":"fnvaWqS7p7ybaoN6g","bibbaseid":"zarrie-claen-onthedecidabilityofverifyingltlpropertiesofgologprograms-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":"On the Decidability of Verifying LTL Properties of Golog Programs","booktitle":"Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14)","year":"2014","publisher":"AAAI Press","abstract":"The high-level action programming language Golog is a useful means for modeling the behavior of autonomous agents such as mobile robots. It relies on a representation given in terms of a logic-based action theory in the Situation Calculus (SC). To guarantee that the possibly non-terminating execution of a Golog program leads to the desired behavior of the agent, it is desirable to (automatically) verify that it satisfies certain requirements given in terms of temporal formulas. However, due to the high (first-order) expressiveness of the Golog language, the verification problem is in general undecidable. In this paper we show that for a fragment of the Golog language defined on top of the decidable logic C\\texttwosuperior, the verification problem for linear time temporal properties becomes decidable, which extends earlier results to a more expressive fragment of the input formalism. Moreover, we justify the involved restrictions on program constructs and action theory by showing that relaxing any of these restrictions instantly renders the verification problem undecidable again.","url":"http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014a.pdf","bibtex":"@INPROCEEDINGS{ZarriessClassen2014a,\n author = {Benjamin Zarrie{\\ss} and Jens Cla{\\ss}en},\n title = {On the Decidability of Verifying {LTL} Properties of\n {G}olog Programs},\n booktitle = {Proceedings of the AAAI 2014 Spring Symposium:\n Knowledge Representation and Reasoning in Robotics\n (KRR'14)},\n year = {2014},\n publisher = {AAAI Press},\n abstract = {The high-level action programming language Golog is a\n useful means for modeling the behavior of autonomous\n agents such as mobile robots. It relies on a\n representation given in terms of a logic-based\n action theory in the Situation Calculus (SC). To\n guarantee that the possibly non-terminating\n execution of a Golog program leads to the desired\n behavior of the agent, it is desirable to\n (automatically) verify that it satisfies certain\n requirements given in terms of temporal\n formulas. However, due to the high (first-order)\n expressiveness of the Golog language, the\n verification problem is in general undecidable. In\n this paper we show that for a fragment of the Golog\n language defined on top of the decidable logic\n C{\\texttwosuperior}, the verification problem for\n linear time temporal properties becomes decidable,\n which extends earlier results to a more expressive\n fragment of the input formalism. Moreover, we\n justify the involved restrictions on program\n constructs and action theory by showing that\n relaxing any of these restrictions instantly renders\n the verification problem undecidable again.},\n url = {http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014a.pdf}\n}\n\n","author_short":["Zarrieß, B.","Claßen, J."],"key":"ZarriessClassen2014a","id":"ZarriessClassen2014a","bibbaseid":"zarrie-claen-onthedecidabilityofverifyingltlpropertiesofgologprograms-2014","role":"author","urls":{"Paper":"http://www.kbsg.rwth-aachen.de/~classen/pub/ZarriessClassen2014a.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["decidability","verifying","ltl","properties","golog","programs","zarrieß","claßen"],"title":"On the Decidability of Verifying LTL Properties of Golog Programs","year":2014}