h1

000229059 001__ 229059
000229059 005__ 20220422221311.0
000229059 0247_ $$2Laufende Nummer$$a32676
000229059 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-48094
000229059 0247_ $$2HSB$$a999910327818
000229059 0247_ $$2OPUS$$a4809
000229059 037__ $$aRWTH-CONV-144035
000229059 041__ $$aEnglish
000229059 082__ $$a004
000229059 1001_ $$0P:(DE-82)IDM01363$$aClaßen, Jens$$b0$$eAuthor$$urwth
000229059 245__ $$aPlanning and verification in the agent language Golog$$cvorgelegt von Jens Claßen$$honline, print
000229059 246_3 $$aPlanen und Verifikation in der Agentensprache Golog$$yGerman
000229059 260__ $$aAachen$$bPublikationsserver der RWTH Aachen University$$c2013
000229059 300__ $$aXIV, 323 S. : graph. Darst.
000229059 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000229059 3367_ $$02$$2EndNote$$aThesis
000229059 3367_ $$2DRIVER$$adoctoralThesis
000229059 3367_ $$2BibTeX$$aPHDTHESIS
000229059 3367_ $$2DataCite$$aOutput Types/Dissertation
000229059 3367_ $$2ORCID$$aDISSERTATION
000229059 500__ $$aZsfassung in dt. und engl. Sprache
000229059 502__ $$aAachen, Techn. Hochsch., Diss., 2013$$gFak01$$o2013-04-26
000229059 5203_ $$aDie 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.$$lger
000229059 520__ $$aThe 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.$$leng
000229059 591__ $$aGermany
000229059 650_7 $$2SWD$$aKünstliche Intelligenz
000229059 650_7 $$2SWD$$aWissensrepräsentation
000229059 650_7 $$2SWD$$aSchlussfolgern
000229059 650_7 $$2SWD$$aAutomatische Handlungsplanung
000229059 650_7 $$2SWD$$aProgrammverifikation
000229059 653_7 $$aInformatik
000229059 653_7 $$2eng$$aartificial intelligence
000229059 653_7 $$2eng$$aknowledge representation
000229059 653_7 $$2eng$$areasoning
000229059 653_7 $$2eng$$aplanning
000229059 653_7 $$2eng$$aprogram verification
000229059 7001_ $$0P:(DE-82)000876$$aLakemeyer, Gerhard$$b1$$eThesis advisor
000229059 8564_ $$uhttps://publications.rwth-aachen.de/record/229059/files/4809.pdf
000229059 909CO $$ooai:publications.rwth-aachen.de:229059$$pVDB$$pdriver$$purn$$popen_access$$popenaire$$pdnbdelivery
000229059 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000229059 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x0
000229059 9201_ $$0I:(DE-82)121920_20140620$$k121920$$lLehr- und Forschungsgebiet Informatik 5 (Wissensbasierte Systeme)$$x1
000229059 961__ $$c2014-05-23$$x2014-01-22$$z2012-02-20
000229059 970__ $$aHT017901468
000229059 9801_ $$aFullTexts
000229059 980__ $$aphd
000229059 980__ $$aI:(DE-82)120000_20140620
000229059 980__ $$aI:(DE-82)121920_20140620
000229059 980__ $$aVDB
000229059 980__ $$aUNRESTRICTED
000229059 980__ $$aConvertedRecord
000229059 980__ $$aFullTexts