Skip to main content
SpringerLink
Log in
SpringerLink
Log in

The Timestamp of Timed Automata

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

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

Abstract

Let \(\mathrm {eNTA}\) be the class of non-deterministic timed automata with silent transitions. Given \(A \in \mathrm {eNTA}\), we effectively compute its timestamp: the set of all pairs (time value, action) of all observable timed traces of A. We show that the timestamp is eventually periodic and that one can compute a simple deterministic timed automaton with the same timestamp as that of A. As a consequence, we have a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for \(\mathrm {eNTA}\). We also show that the language of A is periodic with respect to suffixes.

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 EPUB and 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

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1–2), 253–273 (1999). https://doi.org/10.1016/S0304-3975(97)00173-4

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Kurshan, R.P., Viswanathan, M.: Membership questions for timed and hybrid automata. In: Real-Time Systems Symposium, pp. 254–263 (1998). https://doi.org/10.1109/REAL.1998.739751

  4. 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). https://doi.org/10.1007/978-3-540-30080-9_1

    Chapter  MATH  Google Scholar 

  5. Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48983-5_6

    Chapter  MATH  Google Scholar 

  6. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: ICALP (2), pp. 43–54 (2009). https://doi.org/10.1007/978-3-642-02930-1_4

    Chapter  Google Scholar 

  7. Beauquier, D.: Pumping lemmas for timed automata. In: Nivat, M. (ed.) FoSSaCS 1998. LNCS, vol. 1378, pp. 81–94. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053543

    Chapter  Google Scholar 

  8. Bérard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Inform. 36(2–3), 145–182 (1998). https://doi.org/10.3233/FI-1998-36233

    Article  MathSciNet  MATH  Google Scholar 

  9. Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2–3), 291–345 (2004). https://doi.org/10.1016/j.tcs.2004.04.003

    Article  MathSciNet  MATH  Google Scholar 

  10. 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). https://doi.org/10.1007/BFb0028779

    Chapter  Google Scholar 

  11. Chen, T., Han, T., Katoen, J., Mereacre, A.: Reachability probabilities in Markovian timed automata. In: CDC-ECC, pp. 7075–7080 (2011). https://doi.org/10.1109/CDC.2011.6160992

  12. Choffrut, C., Goldwurm, M.: Timed automata with periodic clock constraints. J. Autom. Lang. Comb. 5(4), 371–403 (2000). https://doi.org/10.25596/jalc-2000-371

    Article  MathSciNet  MATH  Google Scholar 

  13. Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 242–257. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_18

    Chapter  MATH  Google Scholar 

  14. Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Methods Syst. Des. 1(4), 385–415 (1992). https://doi.org/10.1007/BF00709157

    Article  MATH  Google Scholar 

  15. 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). https://doi.org/10.1007/BFb0054180

    Chapter  Google Scholar 

  16. Finkel, O.: Undecidable problems about timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 187–199. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_14

    Chapter  MATH  Google Scholar 

  17. Haase, C., Ouaknine, J., Worrell, J.: On the relationship between reachability problems in timed and counter automata. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 54–65. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33512-9_6

    Chapter  MATH  Google Scholar 

  18. Henzinger, T.A., Prabhu, V.S.: Timed alternating-time temporal logic. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 1–17. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_1

    Chapter  Google Scholar 

  19. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  20. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1–2), 134–152 (1997). https://doi.org/10.1007/s100090050010

    Article  Google Scholar 

  21. Lorber, F., Rosenmann, A., Nickovic, D., Aichernig, B.K.: Bounded determinization of timed automata with silent transitions. Real Time Syst. 53(3), 291326 (2017). https://doi.org/10.1007/s11241-017-9271-x

    Article  MATH  Google Scholar 

  22. Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 496–510. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_33

    Chapter  Google Scholar 

  23. Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap. In: LICS, pp. 54–63 (2004). https://doi.org/10.1109/LICS.2004.1319600

  24. Ouaknine, J., Worrell, J.: Towards a theory of time-bounded verification. In: ICALP (2), pp. 22–37 (2010). https://doi.org/10.1007/978-3-642-14162-1_3

    Chapter  Google Scholar 

  25. Rosenmann, A.: The timestamp of timed automata. arXiv abs/1412.5669v4 (2019). http://arxiv.org/abs/1412.5669

  26. Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Des. 18(1), 25–68 (2001). https://doi.org/10.1023/A:1008734703554

    Article  MATH  Google Scholar 

  27. Wang, F.: Efficient verification of timed automata with BDD-like data structures. STTT 6(1), 77–97 (2004). https://doi.org/10.1007/s10009-003-0135-4

    Article  Google Scholar 

  28. Wozna, B., Zbrzezny, A., Penczek, W.: Checking reachability properties for timed automata via SAT. Fundam. Inform. 55(2), 223–241 (2003)

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

This research was partly supported by the Austrian Science Fund (FWF) Project P29355-N35.

Author information

Authors and Affiliations

  1. Graz University of Technology, Steyrergasse 30, 8010, Graz, Austria

    Amnon Rosenmann

Authors
  1. Amnon Rosenmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Amnon Rosenmann .

Editor information

Editors and Affiliations

  1. Université Paris 13, Villetaneuse, France

    Étienne André

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Rosenmann, A. (2019). The Timestamp of Timed Automata. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation