Minimierung und effiziente Algorithmen für erkennende Homomorphismen über omega-regulären Sprachen

Abstract

Automaten über unendlichen Wörtern sind ein wichtiges Werkzeug für die Modellierung nicht-terminierender Systeme. Häufig werden Systemspezifikationen und Systemeigenschaften durch sogenannte Büchi-Automaten beschrieben, da in dieser Darstellung viele Entscheidbarkeitsfragen einfach beantwortet werden können. Eine Schwierigkeit bei der Handhabung von Büchi-Automaten ist jedoch die Komplexität der Komplementbildung und der Minimierung; zwei Operationen, die in der Praxis bei der Überführung von logischen Spezifikationen in Automaten benötigt werden. Homomorphismen zwischen freien und endlichen Halbgruppen sind ein alternativer Formalismus, um die Klasse der von Büchi-Automaten akzeptierten Sprachen, die sogenannten omega-regulären Sprachen, zu beschreiben. Dort sind, im Gegensatz zu Büchi-Automaten, die Komplementierung und die Minimierung mit geringem Berechnungsaufwand möglich. In dieser Arbeit werden zunächst grundlegende Algorithmen für verschiedene Operationen und Entscheidbarkeitsprobleme auf erkennenden Homomorphismen erarbeitet. Anschließend wird der Einsatz von Homomorphismen in der Praxis getestet.