Counter Machines: Decidable Properties and Applications to Verification Problems

  • Oscar H. Ibarra
  • Jianwen Su
  • Zhe Dang
  • Tevfik Bultan
  • Richard Kemmerer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


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.


Parameterized Constant Safety Property Defense Advance Research Project Agency Reachability Problem Defense Advance Research Project Agency 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur and D. Dill. “A theory of timed automata,” Theo. Comp. Sci., 126(2):183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    B. Baker and R. Book. “Reversal-bounded multipushdown machines,” J.C.S.S., 8:315–332, 1974.zbMATHMathSciNetGoogle Scholar
  3. 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. 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. 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. 6.
    Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. “Past machines,” in preparation.Google Scholar
  7. 7.
    J. Esparza. “Decidability of model checking for infinite-state concurrent systems,” Acta Informatica. 34(2):85–107, 1997.CrossRefMathSciNetGoogle Scholar
  8. 8.
    E. M. Gurari and O. H. Ibarra. “Simple counter machines and number-theoretic problems,” J.C.S.S., 19:145–162, 1979.zbMATHMathSciNetGoogle Scholar
  9. 9.
    O. H. Ibarra. “Reversal-bounded multicounter machines and their decision problems,” J. ACM, 25:116–133, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    O. H. Ibarra, T. Jiang, N. Tran, and H. Wang. “New decidability results concerning two-way counter machines,” SIAM J. Comput., 24(1):123–137, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Y. Matijasevic. “Enumerable sets are Diophantine,” Soviet Math. Dokl, 11:354–357, 1970.Google Scholar
  12. 12.
    M. Minsky. “Recursive unsolvability of Post’s problem of Tag and other topics in the theory of Turing machines.” Ann. of Math., 74:437–455, 1961.CrossRefMathSciNetGoogle Scholar
  13. 13.
    R. Parikh. “On context-free languages,” J. ACM, 13:570–581, 1966.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    L. G. Valiant and M. S. Paterson. “Deterministic one-counter automata,” J. C.S.S., 10:340–350, 1975.zbMATHMathSciNetGoogle Scholar
  15. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Oscar H. Ibarra
    • 1
  • Jianwen Su
    • 1
  • Zhe Dang
    • 1
  • Tevfik Bultan
    • 1
  • Richard Kemmerer
    • 1
  1. 1.Department of Computer ScienceUniversity of CaliforniaSanta BarbaraUSA

Personalised recommendations