h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Planning and verification in the agent language Golog = Planen und Verifikation in der Agentensprache Golog



Verantwortlichkeitsangabevorgelegt von Jens Claßen

ImpressumAachen : Publikationsserver der RWTH Aachen University 2013

UmfangXIV, 323 S. : graph. Darst.


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

  1. Fachgruppe Informatik (120000)
  2. Lehr- und Forschungsgebiet Informatik 5 (Wissensbasierte Systeme) (121920)

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:
Download fulltext PDF

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
English

Interne Identnummern
RWTH-CONV-144035
Datensatz-ID: 229059

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
121920

 Record created 2014-07-16, last modified 2022-04-22


Fulltext:
Download fulltext PDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)