 A finite automaton has a finite number of states, including a start state and at least one accepting state. It starts scanning a word at the leftmost symbol in the start state, and at each step it moves one symbol to the right and enters a (possibly) new state, according to a given transition function. If it can move along the whole word ending in an accepting state, the word is accepted. The application of automata theory to generalized quantifiers was initiated in van Benthem (1986) (Ch. 7, “Semantic automata”). It is easy to construct a finite automaton recognizing \(\forall\) (or \(\forall{^{\text{rel}}}=\) all), i.e., checking that w consists only of 1’s: just remain in the start state = accepting state as long as 1’s are encountered, but go to a rejecting state as soon as a 0 is scanned, and remain there whatever is encountered afterwards. A slightly more complex automaton recognizes \(Q_{\text{even}}\): again there are two states, a start state = the accepting state and a rejecting state, and this time remain in the same state when 0’s are scanned, but go to the other state when a 1 is scanned. To end in the accepting state it is then necessary and sufficient that there are an even number of 1’s. This machine essentially uses cycles of length 2, whereas the first example had only 1-cycles. Call an automaton of the latter kind acyclic. Van Benthem showed that the FO-definable quantifiers are exactly the ones accepted by finite automata that are acyclic and permutation  closed.[17]