Eine Technik, die logische Entscheidungsprobleme auf Fragen über endliche oder unendliche Automaten und die sprachtheoretischen Eigenschaften der von diesen Automaten akzeptierten Sprachen reduziert, indem effektive Übersetzungen zwischen Formeln/Modellen und Automaten hergestellt werden, sodass Erfüllbarkeit, Gültigkeit oder Modellprüfung auf Leerheits-, Inklusions- oder Akzeptanzprobleme von Automaten zurückgeführt werden.

Prinzip

Die syntaktischen oder semantischen Bedingungen einer Logik in einen Automaten übersetzen, dessen akzeptierte Sprache genau (oder konservativ) die relevanten Modelle beschreibt, und dann Automatenabschlüsse und Entscheidbarkeitsergebnisse nutzen, um logische Aussagen zu gewinnen.

Demonstration

Entscheidung der Erfüllbarkeit monadischer zweiter Ordnung auf endlichen Bäumen durch Konstruktion eines endlichen Baumautomaten, der genau die Baumkodierungen akzeptiert, die die Formel erfüllen; Leerheit des Automaten bedeutet Unerfüllbarkeit, Nichtleerheit liefert ein Modell.

Fehlanwendung

Zu glauben, für jede Logik oder Formel existiere eine Automatentranslation, ohne Effektivität oder Abschlusseigenschaften zu prüfen, oder den determinisierungsbedingten Explosionsanstieg zu ignorieren und dadurch fehlerhafte Komplexitätsbehauptungen aufzustellen.

Konsequenz

Bei korrekter Anwendung erhält man präzise Entscheidbarkeits- und Komplexitätsgrenzen, konstruktive Gegenmodelle oder Zertifikate sowie einheitliche Beweise, dass verschiedene Entscheidungsprobleme auf Standardautomatenprobleme reduzierbar sind.

Umkehrung

Anstatt Logik auf Automaten zu reduzieren, kann man Automaten als Definition von Logiken betrachten (z. B. MSO und Automatenklassen); diese Umkehrung betont das Beschreiben von Sprachklassen durch logische Formeln statt das Lösen logischer Probleme mittels Automaten.

Abgrenzung

Erfordert effektive, semantikerhaltende Übersetzungen und stützt sich auf Automatenklassen mit entscheidbaren Operationen; ist nicht unmittelbar anwendbar, wenn Modelle sich nicht als Wörter/Bäume darstellen lassen oder die Zielautomatenklasse die nötigen Abschluss-/Entscheidbarkeitseigenschaften nicht besitzt.

Semantische Spannung

Spannung besteht zwischen Ausdrucksstärke und Entscheidbarkeit: Reichere Logiken können nichtreguläre Eigenschaften kodieren, welche die Automatenreduktion zerstören, sowie zwischen konstruktiven, aber kostenintensiven Automatenübersetzungen und proof-theoretischen oder algebraischen Methoden, die Automatenkomplexität vermeiden.

Synthese

Die Automatentheoretische Methode wandelt systematisch logische Erfüllbarkeits- und Modellprobleme in Automaten-Sprachprobleme um; ihre Stärke liegt in effektiven Übersetzungen und Automatenleerheits-/Abschlussresultaten, wodurch algorithmische und Komplexitätssätze für mittels Automaten darstellbare Logiken gewonnen werden.