Reachability Problems for Dense Counter Machines
Gaoyan Xie, Zhe Dang, Óscar H. Ibarra, Pierluigi San Pietro · 2003
We generalize the traditional definition of a multicounter machine (where the counters, which can only assume nonnegative integer values, can be incremented/decremented by 1 and tested for zero) by allowing the machine the additional ability to increment/decrement the counters by a non- deterministically chosen fractional amount between 0 and 1 (the may be different at each step and need not be the same for all counters). We show that, under some restrictions on counter behavior, the binary reachability set of such a machine is definable in the (decidable) additive theory of the reals and integers. There are applications of this result in verification, and we give an example in the paper. We also extend the notion of language to semilinear language and show its connection to a restricted class of dense multicounter automata.