Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2001: FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science pp 132–143Cite as

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

Extended Abstract

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2245))

Abstract

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.

Supported in part by NSF grant IRI-9700370

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur and D. Dill, “The theory of timed automata,” TCS, 126(2):183–236, 1994

    Article  MATH  MathSciNet  Google Scholar 

  2. P. Abdulla and B. Jonsson, “Verifying programs with unreliable channels,” Information and Computation, 127(2): 91–101, 1996

    Article  MATH  MathSciNet  Google Scholar 

  3. A. Bouajjani, J. Esparza, and O. Maler. “Reachability analysis of pushdown automata: application to model-Checking,” CONCUR’97, LNCS 1243, pp. 135–150

    Google Scholar 

  4. G. Cece and A. Finkel, “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315

    Google Scholar 

  5. H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279

    Google Scholar 

  6. H. Comon and Y. Jurski, “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257

    Google Scholar 

  7. Z. Dang, “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517

    Google Scholar 

  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–84

    Google Scholar 

  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–539

    Google Scholar 

  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, 1999

    Google Scholar 

  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, 2000

    Google Scholar 

  12. Z. Dang, P. San Pietro, and R. A. Kemmerer, “On Presburger Liveness of Discrete Timed Automata,” STACS’01, LNCS 2010, pp. 132–143

    Google Scholar 

  13. A. Finkel and G. Sutre. “Decidability of Reachability Problems for Classes of Two Counter Automata,” STACS’00, LNCS 1770, pp. 346–357

    Google Scholar 

  14. A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97

    Google Scholar 

  15. O. H. Ibarra, “Reversal-bounded multicounter machines and their decision problems,” J.ACM, 25 (1978) 116–133

    Article  MATH  MathSciNet  Google Scholar 

  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, 2000

    Google Scholar 

  17. O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001

    Google Scholar 

  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–435

    Google Scholar 

  19. G. Kreisel and J. L. Krevine, “Elements of Mathematical Logic,” North-Holland, 1967

    Google Scholar 

  20. K. L. McMillan. “Symbolic model-checking-an approach to the state explosion problem,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992

    Google Scholar 

  21. W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,” Acta Informatica, 29(6/7): 499–522, 1992

    Article  MATH  MathSciNet  Google Scholar 

  22. W. Pugh, “TheOmega test: a fast and practical integer programming algorithm for dependence analysis,” Communications of the ACM, 35(8): 102–114, 1992

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science, Washington State University, 99164, Pullman, WA

    Zhe Dang

  2. Department of Computer Science, University of California, 93106, Santa Barbara, CA

    Oscar H. Ibarra

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italia

    Pierluigi San Pietro

Authors
  1. Zhe Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oscar H. Ibarra
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pierluigi San Pietro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, 560012, Bangalore, India

    Ramesh Hariharan  & V. Vinay  & 

  2. Chennai Mathematical Institute, 92 G.N. Chetty Road, 600 017, Chennai, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dang, Z., Ibarra, O.H., Pietro, P.S. (2001). Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter. In: Hariharan, R., Vinay, V., Mukund, M. (eds) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2001. Lecture Notes in Computer Science, vol 2245. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45294-X_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-45294-X_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43002-5

  • Online ISBN: 978-3-540-45294-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation