Paritätsautomat

in der Automatentheorie ein Automat, der auf unendlichen Wörtern arbeitet

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.[1]

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.[2]

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.[3][4]

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.[4]

Ein Paritätsautomat kann allein durch Änderung der Akzeptanzkomponente in äquivalente Rabin-, Streett- und Muller-Automaten überführt werden.[4]

Ein Büchi-Automat kann als Paritätsautomat, dessen Prioritätsfunktion nur auf 0 und 1 abbildet, betrachtet werden.[5]

Einzelnachweise

Bearbeiten
  1. Andrzej Włodzimierz Mostowski: Regular expressions for infinite trees and a standard form of automata. Springer, doi:10.1007/3-540-16066-3_15.
  2. Berndt Farwer: ω-Automata. 2002, S. 10, doi:10.1007/3-540-36387-4_1.
  3. Nir Piterman: From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. 2007, S. 5, doi:10.48550/arXiv.0705.2205.
  4. a b c 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.
  5. Carsten Fritz: Simulation-based simplification of omega-automata. 2005, S. 117.