h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@PHDTHESIS{Claen:229059,
      author       = {Claßen, Jens},
      othercontributors = {Lakemeyer, Gerhard},
      title        = {{P}lanning and verification in the agent language {G}olog},
      address      = {Aachen},
      publisher    = {Publikationsserver der RWTH Aachen University},
      reportid     = {RWTH-CONV-144035},
      pages        = {XIV, 323 S. : graph. Darst.},
      year         = {2013},
      note         = {Zsfassung in dt. und engl. Sprache; Aachen, Techn.
                      Hochsch., Diss., 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'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 statespace. Similar
                      to other forms of reasoning in the Situation Calculus, our
                      verification methods ultimately reduce to classical
                      first-order theorem proving.},
      keywords     = {Künstliche Intelligenz (SWD) / Wissensrepräsentation
                      (SWD) / Schlussfolgern (SWD) / Automatische Handlungsplanung
                      (SWD) / Programmverifikation (SWD)},
      cin          = {120000 / 121920},
      ddc          = {004},
      cid          = {$I:(DE-82)120000_20140620$ / $I:(DE-82)121920_20140620$},
      typ          = {PUB:(DE-HGF)11},
      urn          = {urn:nbn:de:hbz:82-opus-48094},
      url          = {https://publications.rwth-aachen.de/record/229059},
}