Counter Machines and Verification Problems
- Ibarra, Oscar H.
- Su, Jianwen
- Dang, Zhe
- Bultan, Tevfik
- Kemmerer, Richard A.
DOIAbstract
AbstractWe 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 (bi...
Add to ORKG