Counter Machines: Decidable Properties and Applications to Verification Problems
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+9D2 < 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.
KeywordsParameterized Constant Safety Property Defense Advance Research Project Agency Reachability Problem Defense Advance Research Project Agency
Unable to display preview. Download preview PDF.
- 3.H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” Proc. Int. Conf. on Computer Aided Verification, pp. 268–279, 1998.Google Scholar
- 4.Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. “Decidable approximations on discrete clock machines with parameterized durations,” in preparation.Google Scholar
- 5.Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. “Binary reachability analysis of discrete pushdown timed automata,” to appear in CAV 2000.Google Scholar
- 6.Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. “Past machines,” in preparation.Google Scholar
- 11.Y. Matijasevic. “Enumerable sets are Diophantine,” Soviet Math. Dokl, 11:354–357, 1970.Google Scholar
- 15.P. Wolper and B. Boigelot. “Verifying systems with infinite but regular state spaces,” Proc. 10th Int. Conf. on Computer Aided Verification, pp. 88–97, 1998.Google Scholar