Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter

Extended Abstract
  • Zhe Dang
  • Oscar H. Ibarra
  • Pierluigi San Pietro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


We investigate the Presburger liveness problems for nondeterministic reversal-bounded multicounter machines with a free counter (NCMFs). We show the following: - The ∃-Presburger-i.o. problem and the ∃-Presburger-eventual problem are both decidable. So are their duals, the ∀-Presburger-almost-always problem and the ∀-Presburger-always problem. - The ∀-Presburger-i.o. problem and the ∀-Presburger-eventual problem are both undecidable. So are their duals, the ∃-Presburger-almost-always problem and the ∃-Presburger-always problem.

These results can be used to formulate a weak form of Presburger linear temporal logic and developits model-checking theories for NCMFs. They can also be combined with [12] to study the same set of liveness problems on an extended form of discrete timed automata containing, besides clocks, a number of reversalbounded counters and a free counter.


Model Check Mode Vector Disjunctive Normal Form Reachability Problem Time Automaton 
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, “The theory of timed automata,” TCS, 126(2):183–236, 1994zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    P. Abdulla and B. Jonsson, “Verifying programs with unreliable channels,” Information and Computation, 127(2): 91–101, 1996zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    A. Bouajjani, J. Esparza, and O. Maler. “Reachability analysis of pushdown automata: application to model-Checking,” CONCUR’97, LNCS 1243, pp. 135–150Google Scholar
  4. 4.
    G. Cece and A. Finkel, “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315Google Scholar
  5. 5.
    H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279Google Scholar
  6. 6.
    H. Comon and Y. Jurski, “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257Google Scholar
  7. 7.
    Z. Dang, “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517Google Scholar
  8. 8.
    Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su, “Binary Reachability Analysis of Discrete Pushdown Timed Automata,” CAV’00, LNCS 1855, pp. 69–84Google Scholar
  9. 9.
    Z. Dang, O. H. Ibarra and R. A. Kemmerer, “Decidable Approximations on Generalized and Parameterized Discrete Timed Automata,” COCOON’01, LNCS 2108, pp. 529–539Google Scholar
  10. 10.
    Z. Dang and R. A. Kemmerer, “Using the ASTRAL model checker to analyze Mobile IP,” Proceedings of the Twenty-first International Conference on Software Engineering (ICSE’99), pp. 132–141, IEEE Press, 1999Google Scholar
  11. 11.
    Z. Dang and R. A. Kemmerer, “Three approximation techniques forASTRALsymbolic model checking of infinite state real-time systems,” Proceedings of the Twenty-second International Conference on Software Engineering (ICSE’00), pp. 345–354, IEEE Press, 2000Google Scholar
  12. 12.
    Z. Dang, P. San Pietro, and R. A. Kemmerer, “On Presburger Liveness of Discrete Timed Automata,” STACS’01, LNCS 2010, pp. 132–143Google Scholar
  13. 13.
    A. Finkel and G. Sutre. “Decidability of Reachability Problems for Classes of Two Counter Automata,” STACS’00, LNCS 1770, pp. 346–357Google Scholar
  14. 14.
    A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97 Google Scholar
  15. 15.
    O. H. Ibarra, “Reversal-bounded multicounter machines and their decision problems,” J.ACM, 25 (1978) 116–133zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    O. H. Ibarra, “Reachability and safety in queue systems with counters and pushdown stack,” Proceedings of the International Conference on Implementation and Application of Automata, pp. 120–129, 2000Google Scholar
  17. 17.
    O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001Google Scholar
  18. 18.
    O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer, “Counter Machines: Decidable Properties and Applications to Verification Problems,”, MFCS’00, LNCS 1893, pp. 426–435Google Scholar
  19. 19.
    G. Kreisel and J. L. Krevine, “Elements of Mathematical Logic,” North-Holland, 1967Google Scholar
  20. 20.
    K. L. McMillan. “Symbolic model-checking-an approach to the state explosion problem,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992Google Scholar
  21. 21.
    W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,” Acta Informatica, 29(6/7): 499–522, 1992zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    W. Pugh, “TheOmega test: a fast and practical integer programming algorithm for dependence analysis,” Communications of the ACM, 35(8): 102–114, 1992CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Zhe Dang
    • 1
  • Oscar H. Ibarra
    • 2
  • Pierluigi San Pietro
    • 3
  1. 1.School of Electrical Engineering and Computer ScienceWashington State UniversityPullman
  2. 2.Department of Computer ScienceUniversity of CaliforniaSanta Barbara
  3. 3.Dipartimento di Elettronica e InformazionePolitecnico di MilanoItalia

Personalised recommendations