Consider a universal $\{0,1\}$-$k$-counter machine where each of the $k$ registers has a value in $\{0,1\}$ (as opposed to any non-negative integer in the usual formulation), and there are states $q_1, .., q_f$ with $q_1$ initial and $q_f$ final. The set of instructions are chosen from the following: increment $q_a {+}r_j q_b$ i.e. when in state $q_a$ increment register $r_j$ from $0$ to $1$ and transition to state $q_b$, decrement $q_a {-}r_j q_b$ i.e. similar to before but from $1$ to $0$, and forking from $<q_a; n_1, .., n_k>$ to $<q_b; n_1, .., n_k>$ and $<q_c; n_1, .., n_k>$.
The machine is non-deterministic in the sense that more than one instruction may be applicable to a configuration, and universal because a configuration is accepted iff every branch in the computation tree leads to $<q_f; 0, .., 0>$.
i) What is the name for such a CM ? (surely this machine, or an equivalent formulation, must have been studied..)
ii) What is the complexity lower bound for determining if there is a computation from a given configuration $<q_i; n_1, .., n_k>$ such that every leaf in the computation tree is $<q_f; 0, .., 0>$ ?
EDIT Given a universal $\{0,1\}$-$k$-counter machine C (as per description in question) we can decide if it accepts $w \in \{0,1\}^k$ using a TM that accepts input $<C,w>=n$ in $2^{O(n)}$ time by generating all computation trees of height $1,2, .., 2^k$ ($\leq 2^n$). Thus acceptance can be decided in EXPTIME. What is lacking is the lower bound.
Added MathJax equations