Minimierung von Automaten mit Anwendungen in der Verifikation nichtterminierender Systeme

• Antragsteller: Professor Dr. Thomas Wilke
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2001 bis 2007
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5330154

Ziel des Vorhabens ist die Entwicklung von Verfahren zur Minimierung von Formeln und endlichen Automaten, wie sie bei der Beschreibung nichtterminierender Systeme und der Konstruktion von Werkzeugen zur automatischen Verifikation solcher Systeme verwendet werden. Methodisch steht dabei die Ausnutzung von so genannten Simulationsrelationen zur Zustandsreduzierung im Mittelpunkt. Zentraler Bestandteil von Werkzeugen für die automatische Verifikation nicht terminierender Systeme sind so genannte Model-Checker. Der algorithmische Kern von Model-Checkern wird häufig von automatentheoretischen Methoden gebildet, deren Effizienz die Effizienz des Model-Checkers maßgeblich bestimmt und selbst von der Größe der beteiligten Automaten abhängt. Im Vorhaben soll die bei der Effizienzsteigerung von SPIN verwendete Technik - Zustandsverringerung durch Reduktion nach Simulationsrelationen - aufgegriffen, eingehend studiert, ausgebaut und in andere Kontexte übertragen werden. Insbesondere sollen Simulationsrelationen, die eine stärkere Zustandsreduzierung erlauben, entwickelt werden und Erweiterungen auf alternierende Automaten und Baumautomaten erfolgen.

• DFG-Verfahren: Sachbeihilfen