, and Pierluigi San Pietro ©

Abstract. 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 nondeterministically 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 “semilinear language ” to “dense semilinear language ” and show its connection to a restricted class of dense multicounter automata