h1

%0 Thesis
%A Claßen, Jens
%T Planning and verification in the agent language Golog
%C Aachen
%I Publikationsserver der RWTH Aachen University
%M RWTH-CONV-144035
%P XIV, 323 S. : graph. Darst.
%D 2013
%Z Zsfassung in dt. und engl. Sprache
%Z Aachen, Techn. Hochsch., Diss., 2013
%X 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.
%K Künstliche Intelligenz (SWD)
%K Wissensrepräsentation (SWD)
%K Schlussfolgern (SWD)
%K Automatische Handlungsplanung (SWD)
%K Programmverifikation (SWD)
%F PUB:(DE-HGF)11
%9 Dissertation / PhD Thesis
%U https://publications.rwth-aachen.de/record/229059