Alternating finite automaton

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In automata theory, an alternating finite automaton (AFA) is a nondeterministic finite automaton whose transitions are divided into existential and universal transitions. For example, let A be an alternating automaton.

  • For an existential transition (q, a, q_1 \vee q_2), A nondeterministically chooses to switch the state to either q_1 or q_2, reading a. Thus, behaving like a regular nondeterministic finite automaton.
  • For a universal transition (q, a, q_1 \wedge q_2), A moves to q_1 and q_2, reading a, simulating the behavior of a parallel machine.

Note that due to the universal quantification a run is represented by a run tree. A accepts a word w, if there exists a run tree on w such that every path ends in an accepting state.

A basic theorem states that any AFA is equivalent to a nondeterministic finite automaton (NFA) by performing a similar kind of powerset construction as it is used for the transformation of an NFA to a deterministic finite automaton (DFA). This construction converts an AFA with k states to an NFA with up to 2^k states.

An alternative model which is frequently used is the one where Boolean combinations are represented as clauses. For instance, one could assume the combinations to be in disjunctive normal form so that \{\{q_1\},\{q_2,q_3\}\} would represent q_1 \vee (q_2 \wedge q_3). The state tt (true) is represented by \{\{\}\} in this case and ff (false) by \varnothing. This clause representation is usually more efficient.

Formal Definition[edit]

An alternating finite automaton (AFA) is a 6-tuple, (S(\exists), S(\forall), \Sigma, \delta, P_0, F), where

  • S(\exists) is a finite set of existential states. Also commonly represented as S(\vee).
  • S(\forall) is a finite set of universal states. Also commonly represented as S(\wedge).
  • \ \Sigma is a finite set of input symbols.
  • \ \delta is a set of transition functions to next state (S(\exists) \cup S(\forall)) \times (\Sigma \cup \{ \varepsilon \} ) \to 2^{S(\exists) \cup S(\forall)}.
  • \ P_0 is the initial (start) state, such that P_0 \in S(\exists) \cup S(\forall).
  • \ F is a set of accepting (final) states such that F \subseteq S(\exists) \cup S(\forall).