Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2010: Automated Technology for Verification and Analysis pp 218–232Cite as

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

  • Conference paper

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

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.

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. 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