|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
We study various generalizations of reversalbounded multicounter machines and show that they have decidable emptiness, infiniteness, disjointness, containment, and equivalence problems. The extensions include allowing the machines to perform linearrelation 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 infinitestate transition systems. For example, we show that (binary, forward, and backward) reachability, safety, and invariance are solvable for these machines.