Skip to main content
SpringerLink
Log in

Avoiding Shared Clocks in Networks of Timed Automata

  • Conference paper
CONCUR 2012 – Concurrency Theory (CONCUR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7454))

Included in the following conference series:

Abstract

Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA A 1 ∥ A 2 where A 2 reads some clocks reset by A 1, does there exist a NTA A′1 ∥ A′2 without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of A 2 when in parallel with A 1. Finally, we effectively build A′1 ∥ A′2 when it exists.

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. Akshay, S., Bollig, B., Gastin, P., Mukund, M., Narayan Kumar, K.: Distributed Timed Automata with Independently Evolving Clocks. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 82–97. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Alur, R., Dill, D.: Automata for Modeling Real-Time Systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  3. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Balaguer, S., Chatain, T.: Avoiding shared clocks in networks of timed automata. Rapport de recherche 7990, INRIA (2012)

    Google Scholar 

  5. Balaguer, S., Chatain, T., Haar, S.: A concurrency-preserving translation from time Petri nets to networks of timed automata. FMSD (2012)

    Google Scholar 

  6. Bengtsson, J.E., 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 

  7. Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: 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 

  8. Best, E., Devillers, R.R., Kiehn, A., Pomello, L.: Concurrent bisimulations in Petri nets. Acta Inf. 28(3), 231–264 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed Control with Partial Observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2-3), 291–345 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  11. Bouyer, P., Haddad, S., Reynier, P.-A.: Timed Unfoldings for Networks of Timed Automata. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 292–306. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Boyer, M., Roux, O.H.: On the compared expressiveness of arc, place and transition time Petri nets. Fundam. Inform. 88(3), 225–249 (2008)

    MathSciNet  MATH  Google Scholar 

  13. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A Model-Checking Tool for Real-Time Systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Cassez, F., Chatain, T., Jard, C.: Symbolic Unfoldings for Networks of Timed Automata. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 307–321. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. Jour. of Systems and Software (2006)

    Google Scholar 

  16. Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed Modal Specification - Theory and Tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  17. David, A., Larsen, K.G., Li, S., Nielsen, B.: Timed testing under partial observability. In: ICST, pp. 61–70. IEEE Computer Society (2009)

    Google Scholar 

  18. Dima, C.: Positive and negative results on the decidability of the model-checking problem for an epistemic extension of timed CTL. In: TIME, pp. 29–36. IEEE Computer Society (2009)

    Google Scholar 

  19. Dima, C., Lanotte, R.: Distributed Time-Asynchronous Automata. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 185–200. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. van Glabbeek, R.J., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Inf. 37(4/5), 229–327 (2001)

    Article  MATH  Google Scholar 

  21. Halpern, J.Y., Fagin, R., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995)

    Google Scholar 

  22. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Jour. on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  23. Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27–59 (2005)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

  26. Srba, J.: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 15–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Woźna, B., Lomuscio, A.: A Logic for Knowledge, Correctness, and Real Time. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol. 3487, pp. 1–15. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA & LSV (CNRS & ENS Cachan), Cachan, France

    Sandie Balaguer & Thomas Chatain

Authors
  1. Sandie Balaguer
    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

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK

    Maciej Koutny

  2. Department of Computer Science, University of Leicester, Computer Science Building, University Road, LE1 7RH, Leicester, UK

    Irek Ulidowski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Balaguer, S., Chatain, T. (2012). Avoiding Shared Clocks in Networks of Timed Automata. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32940-1_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32939-5

  • Online ISBN: 978-3-642-32940-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation