Simulation-Based Simplification of omega-Automata, Fachbücher von Carsten Fritz

Das Buch "Simulation-Based Simplification of omega-Automata" bietet eine umfassende Analyse von Simulationsbeziehungen als Heuristiken zur Vereinfachung von Omega-Automaten, die auf unendlichen Zeichenfolgen arbeiten. Der Schwerpunkt liegt auf alternierenden Omega-Automaten, insbesondere solchen, die aus LTL-Formeln abgeleitet sind, was für das Modell-Checking von Bedeutung ist. Die Autoren führen verschiedene Simulationsarten ein, darunter direkte, verzögerte und faire Simulationen für alternierende Büchi-Automaten (ABA). Zudem werden Konstruktionen von Simulationsquotienten für ABA behandelt. Die Ergebnisse werden auf die Übersetzung von propositionalen LTL-Formeln in nichtdeterministische Automaten angewendet. Ein Algorithmus zur Übersetzung von LTL in nichtdeterministische Automaten wird entwickelt, der Simulationsbeziehungen zur Vereinfachung in Echtzeit nutzt. Darüber hinaus wird die verzögerte Simulation auf alternierende Paritätsautomaten (APA) ausgeweitet, und es werden Varianten dieser Beziehung vorgestellt, die für die Quotierung von APA geeignet sind. Das Buch richtet sich an Studierende und Forschende, die sich für die Automatentheorie von LTL interessieren.