Skip to main content
SpringerLink
Log in

What’s Decidable About Parametric Timed Automata?

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2015)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 596))

Abstract

Parametric timed automata (PTA) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After two decades of research on PTA, it is now well-understood that any non-trivial problem studied is undecidable for general PTA. We provide here a survey of decision and computation problems for PTA. On the one hand, bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability. On the other hand, restricting the number of clocks, the use of clocks (compared or not with the parameters), and the use of parameters (e.g., used only as upper or lower bounds) leads to decidability of some problems.

This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002).

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

Notes

  1. 1.

    The names EF, AF, EG, AG were first used for PTA by Jovanović et al.  [25], and come from the CTL syntax.

  2. 2.

    Note that EF-, AF-, EG-, and AG-emptiness are equivalent to AG-, EG-, AF-, EF-universality, respectively.

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Logic 2(3), 388–407 (2001)

    Article  MATH  Google Scholar 

  3. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601. ACM (1993)

    Google Scholar 

  4. André, É., Chatain, Th., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819–836 (2009)

    Google Scholar 

  5. André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. André, É., Lime, D., Roux, O.H.: Integer-complete synthesis for bounded parametric timed automata. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 7–19. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24537-9_2

    Chapter  Google Scholar 

  7. André, É., Lime, D., Roux, O.H.: Decision problems for parametric timed automata (submitted, 2016)

    Google Scholar 

  8. André, É., Markey, N.: Language preservation problems in parametric timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 27–43. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  9. Asarin, E., Mysore, V., Pnueli, A., Schneider, G.: Low dimensional hybrid systems – decidable, undecidable, don’t know. Inf. Comput. 211, 138–159 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  10. Beneš, N., Bezděk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015, Part II. LNCS, vol. 9135, pp. 69–81. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  11. Bérard, B., Haddad, S., Jovanović, A., Lime, D.: Parametric interrupt timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 59–69. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 1–18. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Meth. Syst. Des. 35(2), 121–151 (2009)

    Article  MATH  Google Scholar 

  14. Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: complexity and fixed points. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55–70. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Bruyère, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Logical Meth. Comput. Sci. 3(1: 7), 1–30 (2007)

    Google Scholar 

  16. Bundala, D., Ouaknine, J.: Advances in parametric real-time reasoning. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 123–134. Springer, Heidelberg (2014)

    Google Scholar 

  17. Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Meth. Syst. Des. 34(1), 59–81 (2009)

    Article  MATH  Google Scholar 

  18. Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208–213 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  19. Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: International Computer Music Conference (2013)

    Google Scholar 

  20. Fribourg, L., Lesens, D., Moro, P., Soulat, R.: Robustness analysis for scheduling problems using the inverse method. In: TIME, pp. 73–80. IEEE Computer Society Press (2012)

    Google Scholar 

  21. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  22. Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: Fülöp, Z. (ed.) ICALP 1995. LNCS, vol. 944, pp. 417–428. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  23. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  24. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52–53, 183–220 (2002)

    MathSciNet  Google Scholar 

  25. Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)

    Article  Google Scholar 

  26. Jovanović, A.: Parametric verification of timed systems. Ph.D. thesis , École Centrale Nantes, France (2013)

    Google Scholar 

  27. Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 141–159. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  28. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1–2), 134–152 (1997)

    Article  MATH  Google Scholar 

  29. Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  30. Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, p. 296. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Englewood Cliffs (1967)

    MATH  Google Scholar 

  32. Quaas, K.: MTL-model checking of one-clock parametric timed automata is undecidable. SynCoP. EPTCS 145, 5–17 (2014)

    Article  Google Scholar 

  33. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  34. Wang, T., Sun, J., Wang, X., Liu, Y., Si, Y., Dong, J.S., Yang, X., Li, X.: A systematic study on explicit-state non-zenoness checking for timed automata. IEEE Trans. Softw. Eng. 41(1), 3–18 (2015)

    Article  Google Scholar 

Download references

Acknowledgements

This manuscript benefited from discussions with Didier Lime, Nicolas Markey, and Olivier H. Roux.

Author information

Authors and Affiliations

  1. Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, 93430, Villetaneuse, France

    Étienne André

  2. École Centrale de Nantes, IRCCyN, CNRS, UMR 6597, Nantes, France

    Étienne André

Authors
  1. Étienne André
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Étienne André .

Editor information

Editors and Affiliations

  1. AIST Ikeda, Ikeda,Osaka, Japan

    Cyrille Artho

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

André, É. (2016). What’s Decidable About Parametric Timed Automata?. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2015. Communications in Computer and Information Science, vol 596. Springer, Cham. https://doi.org/10.1007/978-3-319-29510-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29510-7_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29509-1

  • Online ISBN: 978-3-319-29510-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation