Efficient On-the-Fly Emptiness Check for Timed Büchi Automata | SpringerLink
Skip to main content
Springer Nature Link
Log in

Efficient On-the-Fly Emptiness Check for Timed Büchi Automata

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6252))

  • 549 Accesses

Abstract

The Büchi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The solution to this problem amounts to searching for a cycle in the so-called zone graph of the automaton. Since non-Zenoness cannot be verified directly from the zone graph, additional constructions are required. In this paper, it is shown that in many cases, non-Zenoness can be ascertained without extra constructions. An on-the-fly algorithm for the non-emptiness problem, using an efficient non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported and the results are seen to be promising.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G., Haakansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST 2006, pp. 125–126 (2006)

    Google Scholar 

  4. Bérard, B., Bouyer, B., Petit, A.: Analysing the pgm protocol with UPPAAL. Int. Journal of Production Research 42(14), 2773–2791 (2004)

    Article  Google Scholar 

  5. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time petri nets. In: IFIP Congress, pp. 41–46 (1983)

    Google Scholar 

  6. Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: RTSS 1997, p. 25 (1997)

    Google Scholar 

  7. Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004)

    Article  MATH  Google Scholar 

  8. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a mode-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  12. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient emptiness check for timed büchi automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010)

    Google Scholar 

  13. Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174–190. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)

    Google Scholar 

  15. Tripakis, S.: Checking timed büchi emptiness on simulation graphs. ACM Transactions on Computational Logic 10(3) (2009)

    Google Scholar 

  16. Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed büchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267–292 (2005)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LaBRI (Université de Bordeaux - CNRS), France

    Frédéric Herbreteau & B Srivathsan

Authors
  1. Frédéric Herbreteau
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. B Srivathsan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Paris, 75205, Paris, France

    Ahmed Bouajjani

  2. National University of Singapore, Republic of Singapore

    Wei-Ngan Chin

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Herbreteau, F., Srivathsan, B. (2010). Efficient On-the-Fly Emptiness Check for Timed Büchi Automata. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15643-4_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15642-7

  • Online ISBN: 978-3-642-15643-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation