# 22.2 Paired Counter Automata

Consider a DFA $$A$$ together with $$d$$ pairs off counters $$(x_1,y_1),\dots,(x_d,y_d)$$. Each transition of $$A$$ is labelled with an update function for all counters. The update functions for the x-counters are $$id:n\rightarrow n$$ and $$++ : n\rightarrow n+1$$. The update function for the y-counters are $$id:n\rightarrow n$$, $$\times 2:n\rightarrow 2n$$ and $$\times 2+1:n\rightarrow 2n+1$$. An accepting configuration is a configuration in which we are in an accepting state and all the counter pairs have the same value, i.e. $$x_1=y_1,\dots,x_d=y_d$$.

Question: is the emptiness problem for this class of automata decidable?