Skip to main content
SpringerLink
Log in

Symbolic Unfoldings for Networks of Timed Automata

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

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

Abstract

In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Extended symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.

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. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science (TCS) 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Salah, R.B., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Bérard, B., Cassez, F., Haddad, S., Roux, O.H., Lime, D.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Software Eng. 17(3), 259–273 (1991)

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  7. Cassez, F., Chatain, T., Jard, C.: Symbolic Unfoldings for Networks of Timed Automata. Technical Report RI-2006-4, IRCCyN/CNRS, Nantes (May 2006)

    Google Scholar 

  8. Cassez, F., Roux, O.H.: Structural translation from time petri nets to timed automata. Journal of Systems and Software (forthcoming, 2006)

    Google Scholar 

  9. Chatain, T., Jard, C.: Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 125–145. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Esparza, J., Römer, S.: An unfolding algorithm for synchronous products of transition systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 2–20. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)

    Article  MATH  Google Scholar 

  12. Fleischhack, H., Stehno, C.: Computing a finite prefix of a time Petri net. ICATPN, 163–181 (2002)

    Google Scholar 

  13. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. 18th IEEE Real-Time Systems Symposium (RTSS 1997), pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  15. Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 296–311. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  17. Merlin, P.M., Farber, D.J.: Recoverability of communication protocols – implications of a theorical study. IEEE Transactions on Communications 24 (1976)

    Google Scholar 

  18. Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431–446. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Aura, T., Lilius, J.: A causal semantics for time petri nets. Theoretical Computer Science 1–2(243), 409–447 (2000)

    Article  MathSciNet  Google Scholar 

  20. Yoneda, T., Schlingloff, B.-H.: Efficient verification of parallel real-time systems. Formal Methods in System Design 2(11), 187–215 (1997)

    Article  Google Scholar 

  21. Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)

    Google Scholar 

  22. Belluomini, W., Myers, C.J.: Verification of timed systems using posets. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 403–415. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS/IRCCyN, Nantes, France

    Franck Cassez

  2. IRISA/INRIA, Campus de Beaulieu, Rennes, France

    Thomas Chatain

  3. IRISA/ENS Cachan, Campus de Kerlann, Bruz, France

    Claude Jard

Authors
  1. Franck Cassez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Chatain
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Claude Jard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2 Avenue de Vignate, Centre Equitation, 38610, Grenoble-Gières, France

    Susanne Graf

  2. Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Wenhui Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cassez, F., Chatain, T., Jard, C. (2006). Symbolic Unfoldings for Networks of Timed Automata. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_24

Download citation

  • DOI: https://doi.org/10.1007/11901914_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-47237-7

  • Online ISBN: 978-3-540-47238-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation