@thesis{Liebenberg2013,
  author      = {Martin Liebenberg},
  title       = {Towards Decidable Verification of Non-Terminating
                  {G}olog Programs},
  school      = {Department of Computer Science, RWTH Aachen
                  University},
  year        = {2013},
  month       = apr,
  advisor     = {Cla{\ss}en, Jens},
  abstract    = {Claßen and Lakemeyer recently introduced algorithms
                  for the verification of temporal properties of
                  non-terminating Golog programs, based on the
                  first-order modal Situation Calculus variant ES, and
                  regression-based reasoning. However, while Golog’s
                  high expressiveness is a desirable feature, it also
                  means that their verification procedures cannot be
                  guaranteed to terminate in general. In this thesis,
                  we address this problem by showing that, for a
                  relevant subset, the verification of non-terminating
                  Golog programs is indeed decidable, which is
                  achieved by means of three restrictions. First, we
                  use the ES variant of a decidable two-variable
                  fragment of the Situation Calculus that was
                  introduced by Gu and Soutchanski. Second, we have to
                  restrict the Golog program to contain ground action
                  only. Finally, we consider special classes of
                  successor state axioms, namely the context-free ones
                  and those that only admit local effects.},
  type        = {Diploma thesis}
}

{"_id":"rAmGBgYDjCcdGfs2X","bibbaseid":"liebenberg-towardsdecidableverificationofnonterminatinggologprograms-2013","author_short":["Liebenberg, M."],"bibdata":{"bibtype":"thesis","type":"Diploma thesis","author":[{"firstnames":["Martin"],"propositions":[],"lastnames":["Liebenberg"],"suffixes":[]}],"title":"Towards Decidable Verification of Non-Terminating Golog Programs","school":"Department of Computer Science, RWTH Aachen University","year":"2013","month":"April","advisor":"Claßen, Jens","abstract":"Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of non-terminating Golog programs, based on the first-order modal Situation Calculus variant ES, and regression-based reasoning. However, while Golog’s high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this thesis, we address this problem by showing that, for a relevant subset, the verification of non-terminating Golog programs is indeed decidable, which is achieved by means of three restrictions. First, we use the ES variant of a decidable two-variable fragment of the Situation Calculus that was introduced by Gu and Soutchanski. Second, we have to restrict the Golog program to contain ground action only. Finally, we consider special classes of successor state axioms, namely the context-free ones and those that only admit local effects.","bibtex":"@thesis{Liebenberg2013,\n author = {Martin Liebenberg},\n title = {Towards Decidable Verification of Non-Terminating\n {G}olog Programs},\n school = {Department of Computer Science, RWTH Aachen\n University},\n year = {2013},\n month = apr,\n advisor = {Cla{\\ss}en, Jens},\n abstract = {Claßen and Lakemeyer recently introduced algorithms\n for the verification of temporal properties of\n non-terminating Golog programs, based on the\n first-order modal Situation Calculus variant ES, and\n regression-based reasoning. However, while Golog’s\n high expressiveness is a desirable feature, it also\n means that their verification procedures cannot be\n guaranteed to terminate in general. In this thesis,\n we address this problem by showing that, for a\n relevant subset, the verification of non-terminating\n Golog programs is indeed decidable, which is\n achieved by means of three restrictions. First, we\n use the ES variant of a decidable two-variable\n fragment of the Situation Calculus that was\n introduced by Gu and Soutchanski. Second, we have to\n restrict the Golog program to contain ground action\n only. Finally, we consider special classes of\n successor state axioms, namely the context-free ones\n and those that only admit local effects.},\n type = {Diploma thesis}\n}\n\n","author_short":["Liebenberg, M."],"key":"Liebenberg2013","id":"Liebenberg2013","bibbaseid":"liebenberg-towardsdecidableverificationofnonterminatinggologprograms-2013","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"thesis","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["towards","decidable","verification","non","terminating","golog","programs","liebenberg"],"title":"Towards Decidable Verification of Non-Terminating Golog Programs","year":2013}