Abstract of Paper

Counter Machines: Decidable Properties and Applications to Verification Problems
by Oscar H. Ibarra, Jianwen Su, Tevfik Bultan, Zhe Dang, and Richard Kemmerer

Abstract:

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-2D_1+9D_2<12$?'', where $x,y$ are
counters and $D_1,D_2$ 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, safety, and invariance are solvable for these machines.