# Counter automata with a bound on the counters?

It is widely known that the emptiness of counter automata is undecidable since two counters are enough to simulate a Turing machine (see the classic book from Hopcroft and Ullman, for example).

However, what happens if we put a bound $$k$$ on the values stored by the counters? In this restricted model, the counters cannot be incremented more than $$k$$.

I think this makes the problem decidable, is this correct? And in this case, what is the complexity? Is there any reference about this problem?

• If the counters are bounded, you can get rid of them by including them as part of the set of states. Commented Sep 23, 2021 at 18:11
• Yes, this makes it easy to prove membership in PSPACE, I suppose. But what about the hardness? Commented Sep 23, 2021 at 18:13
• Can you define the model more precisely? Commented Sep 23, 2021 at 20:41

If the counters are bounded by $$k$$, then the number of possible states is finite, so this is a finite-state machine, and emptiness for finite-state machines is decidable. In particular, if there are $$c$$ counters, each bounded by $$k$$, then there are $$O(k^c)$$ states, so emptiness can be tested in $$O(k^c)$$ time.
Assuming the automaton allows nondeterminism, it is easy to prove that the problem is NP-hard, by a reduction from 3SAT. (Store the value of $$x_i$$ in the $$i$$th counter, selecting its value nondeterministically, then scan over the formula, checking each clause to see if it holds.)