Der Paritätsautomat, auch Parity-Automat, ist in der Automatentheorie ein Automat, der auf unendlichen Wörtern arbeitet. Er ist eine Variante des ω-Automaten. Die von Paritätsautomaten erkannten Sprachen sind die ω-regulären Sprachen. Eingeführt wurde er 1984 von Andrzej Włodzimierz Mostowski.
Definition Bearbeiten
Ein Paritätsautomat ist definiert als ein 5-Tupel mit der endlichen Menge der Zustände , dem Alphabet , der Transitionsfunktion , der Menge der Startzustände und einer Akzeptanzkomponente , für die es verschiedene Definitionen gibt. Weil die Transitionsfunktion auf die Potenzmenge abbildet, ist der Automat nichtdeterministisch. Ein Paritätsautomat ist deterministisch, wenn und für alle und gilt. In diesem Fall kann die Transitionsfunktion als definiert werden.
Sei mit für alle ein unendliches Wort. Ein Lauf für ist eine unendliche Folge mit und für alle . Dabei ist die Menge aller unendlich oft in vorkommenden Zustände.
Die Akzeptanzkomponente kann als Prioritätsfunktion definiert werden. Ein Wort wird dann akzeptiert, wenn dafür ein Lauf existiert, bei dem gerade ist. Alternativ kann auch gefordert werden, dass gerade ist.
Die Akzeptanzkomponente kann auch als Menge mit oder als eine Partition von für eine Zahl , die Index des Automaten genannt wird, definiert werden.
Ein Wort wird dann akzeptiert, wenn dafür ein Lauf existiert, bei dem das minimale mit gerade ist.
Eigenschaften Bearbeiten
Deterministische und nichtdeterministische Paritätsautomaten besitzen die gleiche Ausdrucksstärke. Die von ihnen erkannten Sprachen sind die ω-regulären Sprachen. Sie sind somit äquivalent zu nichtdeterministischen Büchi-Automaten sowie deterministischen und nichtdeterministischen Rabin-, Streett-, Muller- und Generalisierten Büchi-Automaten.
Ein Paritätsautomat kann allein durch Änderung der Akzeptanzkomponente in äquivalente Rabin-, Streett- und Muller-Automaten überführt werden.
Ein Büchi-Automat kann als Paritätsautomat, dessen Prioritätsfunktion nur auf 0 und 1 abbildet, betrachtet werden.
Einzelnachweise Bearbeiten
- Andrzej Włodzimierz Mostowski: Regular expressions for infinite trees and a standard form of automata. Springer, doi:10.1007/3-540-16066-3_15.
- Berndt Farwer: ω-Automata. 2002, S. 10, doi:10.1007/3-540-36387-4_1.
- Nir Piterman: From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. 2007, S. 5, doi:10.48550/arXiv.0705.2205.
- ↑ Orna Kupferman: Automata Theory and Model Checking. In: Edmund Clarke, Thomas Henzinger, Helmut Veith, Roderick Bloem (Hrsg.): Handbook of Model Checking. Springer, 2018, S. 122 ff., doi:10.1007/978-3-319-10575-8_4.
- Carsten Fritz: Simulation-based simplification of omega-automata. 2005, S. 117.