Skip to main content
SpringerLink
Log in

Robustness in Timed Automata

  • Conference paper
Reachability Problems (RP 2013)

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

Included in the following conference series:

Abstract

In this paper we survey several approaches to the robustness of timed automata, that is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.

We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.

Partly supported by ANR project ImpRo (ANR-10-BLAN-0317), by ERC Starting grants EQualIS (FP7-308087) and inVEST (FP7-279499), and by European project Cassting (FP7-601148).

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 49.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. Asarin, E., Bouajjani, A.: Perturbed turing machines and hybrid systems. In: Proc. 16th Annual Symposium on Logic in Computer Science (LICS 2001), pp. 269–278. IEEE Computer Society Press (2001)

    Google Scholar 

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

  3. Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: Proc. 10th International Workshop on Embedded Software (EMSOFT 2010), pp. 229–238. ACM (2010)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Abdulla, P.A., Krčál, P., Yi, W.: Sampled semantics of timed automata. Logical Methods in Computer Science 6(3:14) (2010)

    Google Scholar 

  6. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Alur, R.: Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, Stanford, CA, USA (1991)

    Google Scholar 

  8. Altisen, K., Tripakis, S.: Implementation of timed automata: An issue of semantics or modeling? In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 273–288. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Basset, N., Asarin, E.: Thin and thick timed regular languages. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 113–128. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST 2006), pp. 125–126. IEEE Computer Society Press (2006)

    Google Scholar 

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

    Chapter  Google Scholar 

  12. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: 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 

  13. Bouyer, P., Markey, N., Reynier, P.-A.: Robust model-checking of linear-time properties in timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Bouyer, P., Markey, N., Reynier, P.-A.: Robust analysis of timed automata via channel machines. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 157–171. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Bouyer, P., Markey, N., Sankur, O.: Robust model-checking of timed automata via pumping in channel machines. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 97–112. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Bouyer, P., Markey, N., Sankur, O.: Robust reachability in timed automata: A game-based approach. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 128–140. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  17. Bouyer, P., Markey, N., Sankur, O.: Robust weighted timed automata and games. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 31–46. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Brzozowski, J.A., Seger, C.-J.H.: Advances in asynchronous circuit theory. Bulletin of the European Association of Theoretical Computer Science, EATCS (1991)

    Google Scholar 

  19. Chatterjee, K., Henzinger, T.A., Prabhu, V.S.: Timed parity games: Complexity and robustness. Logical Methods in Computer Science 7(4) (2011)

    Google Scholar 

  20. Cassez, F., Henzinger, T.A., Raskin, J.-F.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. De Wulf, M., Doyen, L., Markey, N., Raskin, J.F.: Robust safety of timed automata. Formal Methods in System Design 33(1-3), 45–84 (2008)

    Article  MATH  Google Scholar 

  22. De Wulf, M., Doyen, L., Raskin, J.-F.: Systematic Implementation of Real-Time Models. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 139–156. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Dima, C.: Dynamical properties of timed automata revisited. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 130–146. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  25. Henzinger, T.A., Raskin, J.-F.: Robust undecidability of timed and hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 145–159. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Krčál, P., Pelánek, R.: On sampled semantics of timed systems. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 310–321. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  27. Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  28. Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  29. Sankur, O.: Shrinktech: A tool for the robustness analysis of timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1006–1012. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  30. Sankur, O., Bouyer, P., Markey, N.: Shrinking timed automata. In: Proc. 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). LIPIcs, vol. 13, pp. 375–386. Leibniz-Zentrum für Informatik (2011)

    Google Scholar 

  31. Sankur, O., Bouyer, P., Markey, N., Reynier, P.-A.: Robust controller synthesis in timed automata. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 546–560. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  32. Swaminathan, M., Fränzle, M., Katoen, J.-P.: The surprising robustness of (closed) timed automata against clock-drift. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) Proc. 5th IFIP International Conference on Theoretical Computer Science (TCS 2008). IFIP, vol. 273, pp. 537–553. Springer, Boston (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, CNRS & ENS Cachan, France

    Patricia Bouyer, Nicolas Markey & Ocan Sankur

  2. Université Libre de Bruxelles, Belgium

    Ocan Sankur

Authors
  1. Patricia Bouyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Markey
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ocan Sankur
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Uppsala University, Sweden

    Parosh Aziz Abdulla

  2. University of Liverpool, Ashton Building, UK

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bouyer, P., Markey, N., Sankur, O. (2013). Robustness in Timed Automata. In: Abdulla, P.A., Potapov, I. (eds) Reachability Problems. RP 2013. Lecture Notes in Computer Science, vol 8169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41036-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41036-9_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41035-2

  • Online ISBN: 978-3-642-41036-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation