look at the entire run ρ. The input is accepted if the corresponding run is in Acc. The set of accepted input ω-words is called the recognized ω-language by the automaton, which is denoted as L(A). The definition of Acc as a subset of Qω is purely formal and not suitable for practice because normally such sets are infinite. The difference between various types of ω-automata (Büchi, Rabin etc.) consists in how they encode certain subsets Acc of Qω as finite sets, and therefore in which such subsets they can encode. Nondeterministic ω-automata Formally, a nondeterministic ω-automaton is a tuple A = (Q,Σ,Δ,Q0,Acc) that consists of the following components: Q is a finite set. The elements of Q are called the states of A. Σ is a finite set called the alphabet of A. Δ is a subset of Q × Σ × Q and is called the transition relation of A. Q0 is a subset of Q, called the initial set of states. Acc is the acceptance condition, a subset of Qω. Unlike a deterministic ω-automaton, which has a transition function δ, the non-deterministic version has a transition relation Δ. Note that Δ can be regarded as a function : Q × Σ → P(Q) from Q × Σ to the power set P(Q). Thus, given a state qn and a symbol an, the next state qn+1 is not necessarily determined uniquely, rather there is a set of possible next states. A run of A on the input α = (a1,a2,a3,...) is any infinite sequence ρ = (r0,r1,r2,...) of states that satisfies the following conditions: r0 is an element of Q0. r1 is an element of Δ(r0,a1). r2 is an element of Δ(r1,a2). ... rn is an element of Δ(rn-1,an). A nondeterministic ω-automaton may admit many different runs on any given input, or none at all. The input is accepted if at least one of the possible runs is accepting. Whether a run is accepting depends only on Acc, as for deterministic ω-automata. Every deterministic ω-automaton can be regarded as a nondeterministic ω-automaton by taking Δ to be the graph of δ. The definitions of runs and acceptance for deterministic ω-automata are then special cases of the nondeterministic cases. Acceptance conditions Acceptance conditions may be infinite sets of ω-words. However, people mostly study acceptance conditions that are finitely representable. The following lists a variety of popular acceptance conditions. Before