State-space reduction of finite automata with applications in the verification of non-terminating systems

• Applicant: Professor Dr. Thomas Wilke
• Subject Area: Theoretical Computer Science
• Term: from 2001 to 2007
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants