Skip to main content
SpringerLink
Log in

Automatic Verification of Multi-queue Discrete Timed Automata

  • Conference paper
  • First Online:
Computing and Combinatorics (COCOON 2003)

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

Included in the following conference series:

Abstract

We propose a new infinite-state model, called the Multi-queue Discrete Timed Automaton MQDTA, which extends Timed Automata with queues, but only has integer-valued clocks. Due to careful restrictions on queue usage, the binary reachability (the set of all pairs of configurations (α, β) of an MQDTA such that α can reach β through zero or more transitions) is effectively semilinear. We then prove the decidability of a class of Presburger formulae defined over the binary reachability, allowing the automatic verification of many interesting properties of a MQDTA. The MQDTA model can be used to specify and verify various systems with unbounded queues, such as a real-time scheduler.

Supported in part by MIUR grants FIRB RBAU01MCAC and COFIN 2001015271.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Abdulla and B. Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241–264, 2002.

    Article  MathSciNet  Google Scholar 

  2. P. Abdulla and A. Nylén. Timed petri nets and bqos. In ICATPN’2001, 22nd Int. Conf. on application and theory of Petri nets, 2001.

    Google Scholar 

  3. R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.

    Article  MATH  MathSciNet  Google Scholar 

  4. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, April 1994.

    Article  MATH  MathSciNet  Google Scholar 

  5. M. Benedikt P. Godefroid and T. Reps. Model checking of unrestricted hierarchical state machines. In ICALP 2001, of LNCS 2076, pp. 652–666. Springer, 2001.

    Google Scholar 

  6. L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi Reghizzi. Multiple pushdown languages and grammars. Int. Journal of Found. of Computer Science, 7:253–291, 1996.

    Article  MATH  Google Scholar 

  7. L. Breveglieri, A. Cherubini, and S. Crespi Reghizzi. Real-time scheduling by queue automata. In FTRTFT’92, vol/ 571 of LNCS, pages 131–148. Springer, 1992.

    Google Scholar 

  8. L. Breveglieri, A. Cherubini, and S. Crespi Reghizzi. Modelling operating systems schedulers with multi-stack-queue grammars. In Fundamentals of Computation Theory, volume 1684 of LNCS, pages 161–172. Springer, 1999.

    Chapter  Google Scholar 

  9. G. Cece and A. Finkel. Programs with quasi-stable channels are effectively recognizable. In CAV’97, volume 1254 of LNCS, pages 304–315. Springer, 1997.

    Google Scholar 

  10. H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV’98, volume 1427 of LNCS, pages 268–279. Springer, 1998.

    Google Scholar 

  11. H. Comon and Y. Jurski. Timed automata and the theory of real numbers. In CONCUR’99, volume 1664 of LNCS, pages 242–257. Springer, 1999.

    Google Scholar 

  12. Zhe Dang. Binary reachability analysis of pushdown timed automata with dense clocks. In CAV’01, volume 2102 of LNCS, pages 506–517. Springer, 2001.

    Google Scholar 

  13. Zhe Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. In CAV’00, LNCS 1855, pages 69–84. Springer, 2000.

    Google Scholar 

  14. S. Ginsburg and E. Spanier. Semigroups, presburger formulas, and languages. Pacific J. of Mathematics, 16:285–296, 1966.

    MATH  MathSciNet  Google Scholar 

  15. P. Godefroid and R. Jagadeesan. Automatic abstraction using generalized model checking. In CAV’02, volume 2404 of LNCS, pages 137–150. Springer, 2002.

    Google Scholar 

  16. B. Grahlmann. The state of pep. In AMAST’98, LNCS 1548, pages 522–526. Springer, 1998.

    Google Scholar 

  17. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, June 1994.

    Article  MATH  MathSciNet  Google Scholar 

  18. R. Parikh. On context-free languages. Journal of the ACM, 13:570–581, 1966.

    Article  MATH  MathSciNet  Google Scholar 

  19. A. Pnueli and E. Shahar. Livenss and acceleraiton in parameterized verification. In CAV’00, volume 1855 of LNCS. Springer, 2000.

    Google Scholar 

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

    Article  Google Scholar 

  21. B. Steffen and O. Burkart. Model checking the full modal mu-calculus for infinite sequential processes. In ICALP’97, volume 1256 of LNCS, pages 419–429.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Pierluigi San Pietro

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

    Zhe Dang

Authors
  1. Pierluigi San Pietro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhe Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Texas at Austin, One University Station, C0500, Austin, TX, 78712, USA

    Tandy Warnow

  2. Department of Computer Science, Montana State University, EPS 357, Bozeman, MT, 59717, USA

    Binhai Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

San Pietro, P., Dang, Z. (2003). Automatic Verification of Multi-queue Discrete Timed Automata. In: Warnow, T., Zhu, B. (eds) Computing and Combinatorics. COCOON 2003. Lecture Notes in Computer Science, vol 2697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45071-8_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-45071-8_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40534-4

  • Online ISBN: 978-3-540-45071-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation