Dense counter machines and verification problems

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 each counter Ci by a nondeterministically chosen fractional amount & between 0 and 1 (δi may be different at each step). Further at each step, the δi's of some counters can be linearly related in that they can be integral multiples of the same fractional δ (e.g., δi = 3δ, δ3 = 6δ). We show that, under some restrictions on counter behavior, the binary reachability set of such a machine is definable in the additive theory of the reals and integers. There arc applications of this result in verification, and we give an example in the paper. We also extend the notion of "semilinear language" to "dense semilin-car language" and show its connection to a restricted class of dense multicounter automata. © Springer-Verlag Berlin Heidelberg 2003.