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, safety, and invariance are solvable for these machines.
CITATION STYLE
Ibarra, O. H., Su, J., Dang, Z., Bultan, T., & Kemmerer, R. (2000). Counter machines: Decidable properties and applications to verification problems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1893, pp. 426–435). Springer Verlag. https://doi.org/10.1007/3-540-44612-5_38
Mendeley helps you to discover research relevant for your work.