2013
Aachen, Techn. Hochsch., Diss., 2013
Zsfassung in dt. und engl. Sprache
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
Tag der mündlichen Prüfung/Habilitation
2013-04-26
Online
URN: urn:nbn:de:hbz:82-opus-48094
URL: https://publications.rwth-aachen.de/record/229059/files/4809.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Künstliche Intelligenz (Genormte SW) ; Wissensrepräsentation (Genormte SW) ; Schlussfolgern (Genormte SW) ; Automatische Handlungsplanung (Genormte SW) ; Programmverifikation (Genormte SW) ; Informatik (frei) ; artificial intelligence (frei) ; knowledge representation (frei) ; reasoning (frei) ; planning (frei) ; program verification (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Die Aktionsprogrammiersprache Golog hat sich als nützliches Mittel zur High-Level-Steuerung autonomer Agenten wie z.B. mobiler Roboter erwiesen. Sie basiert auf dem Situationskalkül, einem Dialekt klassischer Logik der ersten Stufe, welcher zur Darstellung dynamischer Anwendungsdomänen mittels logischer Axiome verwendet wird. Der wahrscheinlich größte Vorteil von Golog ist, daß es die Formulierung von Programmen erlaubt, die den Suchraum möglicher Ausführungspläne auf flexible Weise einschränken. Wenn jedoch generelles Planen benötigt wird, so unterstützt Golog dies zwar prinzipiell, kann sich aber nicht mit Planern auf dem aktuellen Stand der Technik messen, die auf der Plansprache PDDL basieren. Andererseits fehlt Planformalismen und -systemen die Ausdrucksmächtigkeit von Golog, durch die es sich für realistische Szenarien von Agenten mit nur partiellem Weltwissen in dynamischen Umgebungen eignet. In dieser Arbeit schlagen wir daher eine Integration von Golog und Planen vor, bei der während der Ausführung eines Golog-Programms angetroffene Planungssubprobleme an einen PDDL-Planer delegiert werden, und so die Ausdrucksmächtigkeit von Golog mit der Effizienz eines modernen Planers kombiniert wird. Die theoretische Grundlage einer solchen Einbettung wird in Form einer Abbildung zwischen Zustandsaktualisierungen in PDDL und der Progression einer bestimmten Form von Theorien der modalen Situationskalkülvariante ES erbracht. Wir komplementieren diese Ergebnisse mit einer empirischen Evaluierung, die zeigt, daß die Ausstattung eines Golog-Systems mit einem PDDL-Planer tatsächlich eine deutliche Verbesserung der Laufzeitperformanz mit sich bringt. Überdies ist es häufig wünschenswert, vor dem Deployment eines Golog-Programms auf einen Roboter zu verifizieren, daß es bestimmte Voraussetzungen erfüllt, etwa bezüglich Sicherheit, Liveness und Fairness. Da autonome Roboter meist fortwährende Aufgaben erfüllen, sind die entsprechenden Steuerungsprogramme üblicherweise nicht-terminierend. Bislang wurden solche Programme mittels manueller, meta-theoretischer Beweisführungen und komplexer Fixpunkt-Konstruktionen analysiert, was mühsam und fehleranfällig ist. In dieser Arbeit schlagen wir eine Erweiterung der Logik ES vor, die neue Modaloperatoren zur Formulierung temporaler Eigenschaften von Golog-Programmen einführt. Wir präsentieren darüberhinaus Algorithmen zur automatischen Verifikation solcher Eigenschaften, die auf einer systematischen Erforschung des Zustandsraums mithilfe einer neuen Graph-Darstellung von Golog-Programmen basieren. ähnlich wie andere Formen des Reasonings im Situationskalkül können unsere Verifikationsverfahren schlußendlich auf klassisches Theorem-Beweisen in Logik erster Stufe zurückgeführt werden.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.
Fulltext:
PDF
Dokumenttyp
Dissertation / PhD Thesis
Format
online, print
Sprache
English
Interne Identnummern
RWTH-CONV-144035
Datensatz-ID: 229059
Beteiligte Länder
Germany