Counter automaton

A counter automaton is a type of abstract computational model used in the field of computer science, particularly in automata theory and formal verification. It's an extension of finite automata that includes one or more counters, which can be incremented, decremented, or tested for zero. These counters allow the automaton to recognize a wider variety of languages than standard finite automata, which have a limited memory (storing only a finite number of states).