Deduktive Generierung von adaptiven Plänen mit Kontrollstrukturen

Abstract

Die vorliegende Arbeit untersucht die Formalisierung und Anwendung eines generischen, deduktiven Planungsansatzes im Kontext intelligenter Assistenzsysteme. Der Ansatz ermöglicht, unterschiedliche, konsumentengerechte Planerstellungs- und verarbeitungsmethoden zu spezifizieren und zu operationalisieren, die die vielfältigen, notwendigen Planschlussfolgerungsmechanismen für Aktionsplanungsaufgaben in Assistenzsystemen entweder definieren oder zumindest unterstützen. Die Basis des Planungsverfahrens bildet eine temporale Planungslogik, die für ein kompositionales Verfeinerungs-Verfahren eingeführt wird, das es erlaubt, konstruktive Beweise von Planspezifikationen nach planungsspezifischen Gesichtspunkten zu komponieren. Die im Anwendungkontext notwendige Adaptivität von Planerstellung und resultierenden Plänen wird aus Deduktionssicht durch die Verwendung konfigurierbarer Beweisstrategien im Kontext des taktischen Theorembeweisens erreicht. Die Beweisstrategien sind ein direktes Abbild von Planungsstrategien, die an verschiedenen Adaptionspunkten durch die Verwendung entsprechender Verfeinerungsmethoden und allgemeinen oder domänenabhängigen Entscheidungsfunktionen konkretisiert werden können. Für typische Adaptionspunkte, die den Plangenerierungsprozess detailliert in sechs korrelierte Phasen untergliedern, werden ihre Beziehungen zum Verfeinerungsverfahren analysiert und konkrete Adaptionsmerkmale und -kombinationen spezifiziert. Eine Konkretisierung des formalen Modelles zur Kontrollstrategiekonfiguration wird exemplarisch durchgeführt.

This thesis describes the formal model and the application of a generic deductive planning approach investigated in the context of intelligent assistant systems. The approach allows the specification and operationalization of different consumer-oriented plan generating and plan processing methods which either define the manifold plan reasoning mechanisms for action planning tasks in assistant systems or at least support them. Constructive proofs of plan specifications can be composed on the basis of a temporal planning logic and its associated compositional refinement process. Regarding the application context, the necessary adaptation of planning and the resulting plans can be reached from a deductive viewpoint by the use of configurable proof strategies in the sense of tactical theorem proving. The proof strategies result as a direct mapping of planning strategies, which can be refined on different adaptation points by using special methods and general as well as domain specific decision functions. The relations of the plan refinement process to a typical setup of adaptation points, which splits the planning process into six correlated phases, is analyzed and concrete adaptation features and combinations are specified. A sample instantiation of the formal model for configuring control strategies is given.