Planen mit einem Modellprüfer im µ-Kalkül

Zusammenfassung

Beim klassischen Planen wird die Welt als Folge von Situationen angesehen. Eine Folge von Aktionen - ein Plan - überführt eine Startsituation in eine Situation, in der Zielbedingungen erfüllt sind. Die Welt wird modelliert durch Individuen und Prädikate. Operatoren überführen Zuständen in Folgezustände. In diesem Bericht wird das im Rahmen dieser Diplomarbeit entwickelte Planungssystem SaM diskutiert, das Planungsmodellierungen verarbeitet und daraus Planschritte generiert. SaM übersetzt dafür die Planungsmodellierung in einen Dialekt des µ-Kalküls, mit dem Zustandsübergangsmodelle abgebildet werden können. Der Dialekt des µ-Kalküls bildet die Eingabesprache des symbolischen Modellprüfers µcke, der als Planungseinheit von SaM benutzt wird. Die Gegenbeispielsgenerierung von µcke berechnet ein Modell, das die Spezifikation der übersetzten Planungsmodellierung erfüllt. Die Ausgabe der Gegenbeispielsgenerierung wird von SaM zu einem Plan aufbereitet und ausgegeben. SaM bietet eine Planungskomponente, die Arithmetik und konditionale Konstrukte unterstützt, und eine Wissensrepräsentationskomponente, die an Terminologische Logik angelehnt ist. SaM ist ein neuer umfangreicher Planungsansatz, der diese beiden Komponenten integriert. Damit werden dem Planungsbereich Problemdomänen zugänglich, die bisher in diesem Zusammenhang nicht behandelt werden konnten.

Online Kopie

Erhältlich im komprimierten Postscript-Format (mweismue-dipl.ps.gz (307Kb)).

BibTeX Eintrag

@MastersThesis{Weism{\"u}ller98,   author = "Marco Weism{\"u}ller",   title = "{Planen mit einem Modellpr{\"u}fer im $\mu$\/-Kalk{\"u}l,   school = "Universit{\"a}t Ulm",   year = 1998}