Verification of systems containing counters

It is pointed out that systems containing counters have very large and deep state spaces, and the verification of properties on these systems can be very expensive in terms of memory space and computation time. A technique for automatically reducing the state space associated with the system on which some properties that can express both safeness and fairness constraints have to be proved is presented. In particular, a set of conditions upon which some counters can be reduced to three-state, nondeterministic machines is given. The controllers can be simplified by removing the redundancy induced by their interaction with the counter, so that the verification tasks can be more easily performed.<>