Counter automaton

In computer science, more particular in the theory of formal languages, a counter automaton, or counter machine, is a pushdown automaton with only two symbols, formula_1 and the initial symbol in formula_2, the finite set of stack symbols.
Equivalently, a counter automaton is a nondeterministic finite automaton with an additional memory cell that can hold one nonnegative integer number (of unlimited size), which can be incremented, decremented, and tested for being zero.
Properties.
The class of counter automata can recognize a proper superset of the regular and a subset of the deterministic context free languages.
For example, the language formula_3 is a non-regular language accepted by a counter automaton: It can use the symbol formula_1 to count the number of formula_5s in a given input string formula_6 (writing an formula_1 for each formula_5 in formula_6), after that, it can delete an formula_1 for each formula_11 in formula_6.
A two-counter automaton, that is, a two-stack Turing machine with a two-symbol alphabet, can simulate an arbitrary Turing machine.