Streett machine

In automata theory , a branch of computer science , a Streett automaton is a special form of the ω-automaton .

Streett machines for word recognition

A (non-) deterministic Streett automaton is a 5-tuple where: ${\displaystyle {\mathcal {A}}=\left(Q,\Sigma ,\delta ,q_{0},{\mathcal {R}}\right)}$

• ${\displaystyle Q}$ is a finite set of states, the state set
• ${\displaystyle \Sigma }$ is a finite set of symbols, the input alphabet
• ${\displaystyle \delta }$ is the transition function:
  • in the deterministic case with ${\displaystyle \delta \colon Q\times \Sigma \rightarrow Q}$
  • in the non-deterministic case with ${\displaystyle \delta \colon Q\times \Sigma \rightarrow 2^{Q}}$
• ${\displaystyle q_{0}\in Q}$ is the start state
• ${\displaystyle {\mathcal {R}}\subseteq 2^{Q}\times 2^{Q}}$ is a family of pairs of state sets

Here called the power set of . ${\displaystyle 2^{Q}}$ ${\displaystyle Q}$

Acceptance behavior

An infinite word is accepted by the Streett automaton if and only if the following applies for a (deterministic: the) associated infinite path : ${\displaystyle w=a_{1}a_{2}\ldots }$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle \pi =q_{0}\;{\xrightarrow {a_{1}}}\;q_{1}\;{\xrightarrow {a_{2}}}\;q_{2}\;\ldots }$

${\displaystyle \forall (E,F)\in {\mathcal {R}}:\operatorname {Inf} (\pi )\cap F\neq \emptyset \Rightarrow \operatorname {Inf} (\pi )\cap E\neq \emptyset }$, d. H. if a state from is visited infinitely often, then at least one state from the associated state is also visited infinitely often. ${\displaystyle F}$ ${\displaystyle E}$

Alternatively, there is the equivalent acceptance condition . ${\displaystyle \forall (E,F)\in {\mathcal {R}}:\operatorname {Inf} (\pi )\cap E\neq \emptyset \lor \operatorname {Inf} (\pi )\cap F=\emptyset }$

This acceptance condition is dual to the acceptance condition of the Rabin machine .

literature

• Erich Grädel, Wolfgang Thomas, Thomas Wilke (Eds.): Automata, Logics, and Infinite Games. A Guide to Current Research (= Lecture Notes in Computer Science. Vol. 2500). Springer, Berlin et al. 2002, ISBN 3-540-00388-6 .