Forschung

Unendliche Graphen / Verifikation unendlicher Systeme durch Model-Checking

Die automatische Verifkation zustandsbasierter Systeme ist zunächst für Systeme mit endlichem Zustandsraum entwickelt worden. Wir beteiligen uns an den Forschungen, diese Methode auf unendliche Systeme auszudehnen. Dazu werden Klassen von unendlichen Graphen, die endlich darstellbar sind, studiert.

Fragestellungen aus diesem Themenbereich werden auch in dem Projekt Endlich repräsentierte unendliche Graphen - Struktur, Verhalten, Algorithmen untersucht.

Arbeiten hierzu: [Löd02a], [Löd02b], [Cac03], [CW03], [Tho03a], [WT04], [Kar05a].

Verallgemeinerte Automatentheorie

In den Anwendungen der Automatentheorie (besonders für die Modellierung von Informatik-Systemen und in der Programmverifikation) sind allgemeinere Automatenmodelle nötig als nur endliche Automaten über endlichen Wörtern. Diese Verallgeimeinerung kann einerseits das betrachtete Automatenmodell betreffen aber auch die von den Automaten verarbeiteten Strukturen. So werden in unserer Forschungsgruppe z.B. Automaten über Bäumen, Bildern (Matrizen aus Buchstaben), Halbordnungen und allgemeinen Relationalstrukturen untersucht.

Arbeiten hierzu: [MST02], [Tho03b], [ATW03], [KT04], [Kar04], [Kar05a].

Unendliche Spiele und Synthese reaktiver Programme

Unendliche Zweipersonenspiele sind einerseits ein natürliches Modell für nichtterminierende reaktive Systeme, andererseits ein Zugang für viele Probleme des Model-Checking. Eine zentrales Problem ist die automatische Synthese von Controllern (d.h. Implementierungen von Gewinnstrategien). Daneben gibt es auch Anwendungen in der klassichen Logik. Unsere Forschungen haben folgende Ziele:

  • für Spiele über endlichen Zustandsräumen effiziente Gewinnstrategien zu gewinnen (automatische Synthese von Controllern, die nach verschiedenen Kriterien optimal sind),
  • auch für Spiele über unendlichen Zustandsräumen algorithmische Verfahren zu entwicklen, mit denen man Gewinnstrategien generieren kann.

Ausgewählte Arbeiten hierzu: [Tho97d], [Vög00], [Cac02b], [Cac03b], [WHT03], [Wal03], [BSL04].

Automaten und Logik-Systeme, Automaten auf unendlichen Wörtern

Die Bedeutung der Automatentheorie für die Verifikation liegt darin, dass Automaten ein Verbindungsglied zwischen Systembeschreibung und Spezifikation sind. Dies liegt an der Übersetzbarkeit vieler Logik-Systeme in Automaten (u.a. temporale Logiken, modale Logiken, Programmlogiken). Die genaue Kenntnis dieses Zusammenhangs zwischen Logiken und Automaten ist die Grundlage für Fortschritte in der algorithmischen Verifikation. Da die Anwendungen i.a. nicht-terminierende (reaktive) Systeme betreffen, sind Automaten über unendlichen Wörtern (bzw. unendlichen Bäumen) ein zentraler Gegenstand dieser Forschungen.

Arbeiten hierzu: [Tho90a], [Tho99a], [LT00], [CT02].

Softwaretools zur Automatentheorie

In der Forschungsgruppe wurden folgende Tools entwickelt:

  • AMoRE (auf englisch) - grundlegende Algorithmen zu regulären Sprachen einschließlich der algebraischen Theorie regulärer Sprachen;
  • OMEGA (auf englisch) - Plattform für den Test automatentheoretischer Algorithmen in der Theorie unendlicher Spiele (abgeschlossen);
  • GASt (auf englisch) - Plattform für Algorithmen zur Lösung von unendlichen Zwei-Personen-Spielen und der Determinisierung von Büchi-Automaten.

In verschiedenen Diplomarbeiten wird an Ergänzungen dieser Tools gearbeitet: Java-Schnittstelle für AMoRE, Graphische Komponenten für AMoRE, Erweiterung auf Baumautomaten, etc.

Arbeiten hierzu: [SV00b], [MMP+95].

Geschichte und Methodologie der Informatik

Arbeiten hierzu: [ST00], [Tho01].