Detailseite
Projekt
Verifikation Nicht-Terminierender Aktionsprogramme (VERITAS)
Fachliche Zuordnung
Theoretische Informatik
Förderung
Förderung von 2012 bis 2021
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 167839951
Die Aktionssprache GOLOG dient vor allem zur Spezifikation des High-Level-Verhaltens von Agenten, einschließlich mobiler Roboter. Da solche autonomen Systeme typischerweise fortwährenden Aufgaben nachgehen, sind die entsprechenden GOLOG-Programme oft nicht-terminierend. Um sicherzustellen, dass die Programmausführung das beabsichtigte Verhalten erzielt, ist es oft vorteilhaft, die erwünschten (meist temporalen) Eigenschaften formal spezifizieren und dann automatisch verifizieren zu können. Das allgemeine Problem der Verifikation von GOLOG, das die volle Ausdrucksmächtigkeit der Prädikatenlogik erster Stufe unterstützt, ist jedoch unentscheidbar. In der ersten Phase dieses Projekts haben wir interessante Fragmente identifiziert, in denen Verifikation entscheidbar wird, trotzdem aber möglichst viel der ursprünglichen Ausdrucksmächtigkeit von GOLOG beibehalten. In der zweiten Phase beabsichtigen wir die Anwendbarkeit unserer Verifikationsmethoden auf realistischere Szenarios auszuweiten, mit besonderem Augenmerk auf Anwendungen in der Robotik. Insbesondere werden wir über bloße Entscheidbarkeit hinausgehend die praktische Ausführbarkeit untersuchen, Konzepte zur Darstellung stetiger Veränderungen sowie probabilistischer Unsicherheit miteinbeziehen, und den Fall betrachten, dass dynamische Modelle der Umgebung zur Verfügung stehen.
DFG-Verfahren
Forschungsgruppen
Teilprojekt zu
FOR 1513:
Hybrides Schließen in intelligenten Systemen
