discussing the list, let's make the following observation. In the case of infinitely running systems, one is often interested in whether certain behavior is repeated infinitely often. For example, if a network card receives infinitely many ping requests, then it may fail to respond to some of the requests but should respond to an infinite subset of received ping requests. This motivates the following definition: For any run ρ, let Inf(ρ) be the set of states that occur infinitely often in ρ. This notion of certain states being visited infinitely often will be helpful in defining the following acceptance conditions. A Büchi automaton is an ω-automaton A that uses the following acceptance condition, for some subset F of Q: Büchi conditionA accepts exactly those runs ρ for which Inf(ρ) ∩ F is not empty, i.e. there is an accepting state that occurs infinitely often in ρ. A is an ω-automaton A that uses the following acceptance condition, for some set Ω of pairs (Bi,Gi) of sets of states: Rabin condition A accepts exactly those runs ρ for which there exists a pair (Bi,Gi) in Ω such that Bi ∩ Inf(ρ) is empty and Gi ∩ Inf(ρ) is not empty. A Streett automaton is an ω-automaton A that uses the following acceptance condition, for some set Ω of pairs (Bi,Gi) of sets of states: Streett condition A accepts exactly those runs ρ such that for all pairs (Bi,Gi) in Ω, Bi ∩ Inf(ρ) is empty or Gi ∩ Inf(ρ) is not empty. A parity automaton is an automaton A whose set of states is Q = {0,1,2,...,k} for some natural number k, and that has the following acceptance condition: Parity condition A accepts ρ if and only if the smallest number in Inf(ρ) is even. A Muller automaton is an ω-automaton A that uses the following acceptance condition, for a subset F of P(Q) (the power set of Q): Muller conditionA accepts exactly those runs ρ for which Inf(ρ) is an element of F. Every Büchi automaton can be regarded as a Muller automaton. It suffices to replace F by F' consisting of all subsets of Q that contain at least one element of F. Similarly every Rabin, Streett or parity automaton can also be regarded as a Muller automaton. Example The following ω-language L over the alphabet Σ = {0,1}, which can be recognized by a nondeterministic Büchi automaton: L