Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan,
and Richard A. Kemmerer
Counter Machines and Verification Problems
Theoretical Computer Science, Vol. 289, No. 1, Pages 165-189,
October 2002
We study various generalizations of reversal-bounded multicounter
machines and show that they have decidable emptiness, infiniteness,
disjointness, containment, and equivalence problems. The extensions
include allowing the machines to perform linear-relation tests among
the counters and parameterized constants (e.g., "Is 3x
-5y-2D1+9D2<12?", where
x, y are counters, and D1,
D2 are parameterized constants). We believe that
these machines are the most powerful machines known to date for which
these decision problems are decidable. Decidability results for such
machines are useful in the analysis of reachability problems and the
verification/debugging of safety properties in infinite-state
transition systems. For example, we show that (binary, forward, and
backward) reachability and safety are solvable for these machines.