Planning and Verification in the Agent Language Golog

Planning and Verification in the Agent Language Golog. Claßen, J. Ph.D. Thesis, Department of Computer Science, RWTH Aachen University, 2013.

Paper abstract bibtex

The action programming language Golog has proven to be a useful means for the high-level control of autonomous agents such as mobile robots. It is based on the Situation Calculus, a dialect of classical first-order logic, that is used to encode dynamic domains through logical axioms. Perhaps the greatest advantage of Golog is that a user can write programs which constrain the search for an executable plan in a flexible manner. However, when general planning is needed, Golog supports this only in principle, but does not measure up with state-of-the-art planners, most of which are based on the plan language PDDL. On the other hand, planning formalisms and systems lack the expressiveness of Golog that make it suited for realistic scenarios of agents with partial world knowledge acting in dynamic environments. We therefore propose an integration of Golog and planning where planning subtasks encountered during the execution of a Golog program are referred to a PDDL planner, thus combining Golog\textquoterights expressiveness with the efficiency of modern planners. The theoretical justification for such an embedding is provided in the form of relating state updates in PDDL to the progression of a certain form of theories of the modal Situation Calculus variant ES. We complement these results with an empirical evaluation that shows that equipping Golog with a PDDL planner indeed pays off in terms of the runtime performance. Moreover, before deploying a Golog program onto a robot, it is often desirable to verify that certain requirements are met, typical examples including safety, liveness and fairness conditions. Since autonomous robots typically perform open-ended tasks, the corresponding control programs are often non-terminating. Analyzing such programs so far requires manual, meta-theoretic arguments involving complex fixpoint constructions, which is tedious and error-prone. In this thesis, we propose an extension to ES that includes new modal operators to express temporal properties of Golog programs. We then provide algorithms for the automated verification of such properties, relying on a newly introduced graph representation for Golog programs which enables a systematic exploration of the state space. Similar to other forms of reasoning in the Situation Calculus, our verification methods ultimately reduce to classical first-order theorem proving.

@PHDTHESIS{Cla:PHD2013,
  author      = {Jens Cla{\ss}en},
  title       = {Planning and Verification in the Agent Language
                  {G}olog},
  school      = {Department of Computer Science, RWTH Aachen
                  University},
  year        = {2013},
  abstract    = {The action programming language Golog has proven to
                  be a useful means for the high-level control of
                  autonomous agents such as mobile robots. It is based
                  on the Situation Calculus, a dialect of classical
                  first-order logic, that is used to encode dynamic
                  domains through logical axioms. Perhaps the greatest
                  advantage of Golog is that a user can write programs
                  which constrain the search for an executable plan in
                  a flexible manner. However, when general planning is
                  needed, Golog supports this only in principle, but
                  does not measure up with state-of-the-art planners,
                  most of which are based on the plan language
                  PDDL. On the other hand, planning formalisms and
                  systems lack the expressiveness of Golog that make
                  it suited for realistic scenarios of agents with
                  partial world knowledge acting in dynamic
                  environments. We therefore propose an integration of
                  Golog and planning where planning subtasks
                  encountered during the execution of a Golog program
                  are referred to a PDDL planner, thus combining
                  Golog{\textquoteright}s expressiveness with the
                  efficiency of modern planners. The theoretical
                  justification for such an embedding is provided in
                  the form of relating state updates in PDDL to the
                  progression of a certain form of theories of the
                  modal Situation Calculus variant ES. We complement
                  these results with an empirical evaluation that
                  shows that equipping Golog with a PDDL planner
                  indeed pays off in terms of the runtime
                  performance. Moreover, before deploying a Golog
                  program onto a robot, it is often desirable to
                  verify that certain requirements are met, typical
                  examples including safety, liveness and fairness
                  conditions. Since autonomous robots typically
                  perform open-ended tasks, the corresponding control
                  programs are often non-terminating. Analyzing such
                  programs so far requires manual, meta-theoretic
                  arguments involving complex fixpoint constructions,
                  which is tedious and error-prone. In this thesis, we
                  propose an extension to ES that includes new modal
                  operators to express temporal properties of Golog
                  programs. We then provide algorithms for the
                  automated verification of such properties, relying
                  on a newly introduced graph representation for Golog
                  programs which enables a systematic exploration of
                  the state space. Similar to other forms of reasoning
                  in the Situation Calculus, our verification methods
                  ultimately reduce to classical first-order theorem
                  proving.},
  url         = {http://darwin.bth.rwth-aachen.de/opus3/volltexte/2013/4809/}
}

Downloads: 0

{"_id":"jAkpxB49iCMua9uCK","bibbaseid":"claen-planningandverificationintheagentlanguagegolog-2013","author_short":["Claßen, J."],"bibdata":{"bibtype":"phdthesis","type":"phdthesis","author":[{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]}],"title":"Planning and Verification in the Agent Language Golog","school":"Department of Computer Science, RWTH Aachen University","year":"2013","abstract":"The action programming language Golog has proven to be a useful means for the high-level control of autonomous agents such as mobile robots. It is based on the Situation Calculus, a dialect of classical first-order logic, that is used to encode dynamic domains through logical axioms. Perhaps the greatest advantage of Golog is that a user can write programs which constrain the search for an executable plan in a flexible manner. However, when general planning is needed, Golog supports this only in principle, but does not measure up with state-of-the-art planners, most of which are based on the plan language PDDL. On the other hand, planning formalisms and systems lack the expressiveness of Golog that make it suited for realistic scenarios of agents with partial world knowledge acting in dynamic environments. We therefore propose an integration of Golog and planning where planning subtasks encountered during the execution of a Golog program are referred to a PDDL planner, thus combining Golog\\textquoterights expressiveness with the efficiency of modern planners. The theoretical justification for such an embedding is provided in the form of relating state updates in PDDL to the progression of a certain form of theories of the modal Situation Calculus variant ES. We complement these results with an empirical evaluation that shows that equipping Golog with a PDDL planner indeed pays off in terms of the runtime performance. Moreover, before deploying a Golog program onto a robot, it is often desirable to verify that certain requirements are met, typical examples including safety, liveness and fairness conditions. Since autonomous robots typically perform open-ended tasks, the corresponding control programs are often non-terminating. Analyzing such programs so far requires manual, meta-theoretic arguments involving complex fixpoint constructions, which is tedious and error-prone. In this thesis, we propose an extension to ES that includes new modal operators to express temporal properties of Golog programs. We then provide algorithms for the automated verification of such properties, relying on a newly introduced graph representation for Golog programs which enables a systematic exploration of the state space. Similar to other forms of reasoning in the Situation Calculus, our verification methods ultimately reduce to classical first-order theorem proving.","url":"http://darwin.bth.rwth-aachen.de/opus3/volltexte/2013/4809/","bibtex":"@PHDTHESIS{Cla:PHD2013,\n author = {Jens Cla{\\ss}en},\n title = {Planning and Verification in the Agent Language\n {G}olog},\n school = {Department of Computer Science, RWTH Aachen\n University},\n year = {2013},\n abstract = {The action programming language Golog has proven to\n be a useful means for the high-level control of\n autonomous agents such as mobile robots. It is based\n on the Situation Calculus, a dialect of classical\n first-order logic, that is used to encode dynamic\n domains through logical axioms. Perhaps the greatest\n advantage of Golog is that a user can write programs\n which constrain the search for an executable plan in\n a flexible manner. However, when general planning is\n needed, Golog supports this only in principle, but\n does not measure up with state-of-the-art planners,\n most of which are based on the plan language\n PDDL. On the other hand, planning formalisms and\n systems lack the expressiveness of Golog that make\n it suited for realistic scenarios of agents with\n partial world knowledge acting in dynamic\n environments. We therefore propose an integration of\n Golog and planning where planning subtasks\n encountered during the execution of a Golog program\n are referred to a PDDL planner, thus combining\n Golog{\\textquoteright}s expressiveness with the\n efficiency of modern planners. The theoretical\n justification for such an embedding is provided in\n the form of relating state updates in PDDL to the\n progression of a certain form of theories of the\n modal Situation Calculus variant ES. We complement\n these results with an empirical evaluation that\n shows that equipping Golog with a PDDL planner\n indeed pays off in terms of the runtime\n performance. Moreover, before deploying a Golog\n program onto a robot, it is often desirable to\n verify that certain requirements are met, typical\n examples including safety, liveness and fairness\n conditions. Since autonomous robots typically\n perform open-ended tasks, the corresponding control\n programs are often non-terminating. Analyzing such\n programs so far requires manual, meta-theoretic\n arguments involving complex fixpoint constructions,\n which is tedious and error-prone. In this thesis, we\n propose an extension to ES that includes new modal\n operators to express temporal properties of Golog\n programs. We then provide algorithms for the\n automated verification of such properties, relying\n on a newly introduced graph representation for Golog\n programs which enables a systematic exploration of\n the state space. Similar to other forms of reasoning\n in the Situation Calculus, our verification methods\n ultimately reduce to classical first-order theorem\n proving.},\n url = {http://darwin.bth.rwth-aachen.de/opus3/volltexte/2013/4809/}\n}\n\n","author_short":["Claßen, J."],"key":"Cla:PHD2013","id":"Cla:PHD2013","bibbaseid":"claen-planningandverificationintheagentlanguagegolog-2013","role":"author","urls":{"Paper":"http://darwin.bth.rwth-aachen.de/opus3/volltexte/2013/4809/"},"metadata":{"authorlinks":{}}},"bibtype":"phdthesis","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["planning","verification","agent","language","golog","claßen"],"title":"Planning and Verification in the Agent Language Golog","year":2013}