Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2019

29.07.2017 | Regular Paper

What’s decidable about parametric timed automata?

verfasst von: Étienne André

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well understood that any non-trivial problem studied is undecidable for general PTAs. We provide here a survey of decision and computation problems for PTAs. 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. We also put emphasis on open problems. We also discuss formalisms close to parametric timed automata (such as parametric hybrid automata or parametric interrupt timed automata), and we study tools dedicated to PTAs and their extensions.
Vorheriger Artikel Formal specification and implementation of an automated pattern-based parallel-code generation framework
Nächster Artikel Knowledge-based security testing of web applications by logic programming

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The names EF, AF, EG, AG were first used for PTAs in [53], and come from the CTL syntax.
 
2
In general, it can be handful to set \(G= F\); but as not all definitions of PTAs in the literature have accepting locations, we use here the set \(G\) to denote goal locations.
 
3
Note that EF-, AF-, EG-, and AG-emptiness are equivalent to AG-, EG-, AF-, EF-universality, respectively.
 
4
This table is partially inspired by a similar table in [42], improved by adding more dimensions, and of course more recent results.
 
Literatur
1.
Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, R. (eds.) FSTTCS. LNCS, vol. 1530, pp. 245–256. Springer, New York (1998)
2.
3.
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetCrossRefMATH
4.
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems 1992. LNCS, vol. 736, pp. 209–229. Springer, New York (1993)
5.
6.
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Logic 2(3), 388–407 (2001)MathSciNetCrossRefMATH
7.
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601. ACM (1993)
8.
Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13–18, 2004, Revised Lectures. LNCS, vol. 3185, pp. 1–24. Springer, New York (2004)
9.
André, É.: Parametric deadlock-freeness checking timed automata. In: Sampaio, A.C.A., Wang, F. (eds.) ICTAC. LNCS, vol. 9965, pp. 469–478. Springer, New York (2016)
10.
André, É.: What’s decidable about parametric timed automata? In: Artho, C., Ölveczky, P.C. (eds.) FTSCS. Communications in Computer and Information Science, vol. 596, pp. 1–17. Springer, New York (2016)
11.
André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819–836 (2009)MathSciNetMATH
12.
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. LNCS, vol. 7436, pp. 33–36. Springer, New York (2012)
13.
André, É., Lime, D.: Liveness in L/U-parametric timed automata. In: Legay, A., Schneider, K. (eds.) ACSD, pp. 9–18. IEEE, New York (2017)
14.
André, É., Lime, D., Markey, N.: Language preservation problems in parametric timed automata (journal version). Technical report (2016), submitted
15.
André, É., Lime, D., Roux, O.H.: Integer-complete synthesis for bounded parametric timed automata. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP. LNCS, vol. 9058. Springer, New York (2015)
16.
André, É., Lime, D., Roux, O.H.: Decision problems for parametric timed automata. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM (2016), to appear
17.
André, É., Lime, D., Roux, O.H.: On the expressiveness of parametric timed automata. In: Fränzle, M., Markey, N. (eds.) FORMATS (2016), to appear
18.
André, É., Lin, S.W.: Learning-based compositional parameter synthesis for event-recording automata. In: Bouajjani, A., Alexandra, S. (eds.) FORTE. LNCS, vol. 10321, pp. 17–32. Springer, New York (2017)
19.
André, É., Liu, Y., Sun, J., Dong, J.S.: Parameter synthesis for hierarchical concurrent real-time systems. In: Perseil, I., Pouzet, M., Breitman, K. (eds.) ICECCS, pp. 253–262. IEEE Computer Society, Silver Spring (2012)
20.
André, É., Liu, Y., Sun, J., Dong, J.S., Lin, S.W.: PSyHCoS: parameter synthesis for hierarchical concurrent real-time systems. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol. 8044, pp. 984–989. Springer, New York (2013)
21.
André, É., Markey, N.: Language preservation problems in parametric timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS. LNCS, vol. 9268, pp. 27–43. Springer, New York (2015)
22.
André, É., Nguyen, H.G., Petrucci, L., Sun, J.: Parametric model checking timed automata under non-Zenoness assumption. In: Barrett, C., Kahsai, T. (eds.) NFM. Lecture Notes in Computer Science, vol. 10227, pp. 35–51. Springer, New York (2017)
23.
Asarin, E., Mysore, V., Pnueli, A., Schneider, G.: Low dimensional hybrid systems—decidable, undecidable, don’t know. Inf. Comput. 211, 138–159 (2012)MathSciNetCrossRefMATH
24.
Aştefănoaei, L., Bensalem, S., Bozga, M., Cheng, C., Ruess, H.: Compositional parameter synthesis. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) Proceedings of the 21st International Symposium on Formal Methods (FM 2016). Lecture Notes in Computer Science, vol. 9995, pp. 60–68 (2016)
25.
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRef
26.
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, Part II. LNCS, vol. 9135, pp. 69–81. Springer, New York (2015)
27.
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. LNCS, vol. 3829, pp. 211–225. Springer, New York (2005)
28.
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: The expressive power of time Petri nets. Theor. Comput. Sci. 474, 1–20 (2013)MathSciNetCrossRefMATH
29.
Bérard, B., Haddad, S., Jovanovic, A., Lime, D.: Interrupt timed automata with auxiliary clocks and parameters. Fundamenta Informormatica 143(3–4), 235–259 (2016)MathSciNetCrossRefMATH
30.
Bérard, B., Haddad, S., Picaronny, C., Din, M.S.E., Sassolas, M.: Polynomial interrupt timed automata. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds.) RP. LNCS, vol. 9328, pp. 20–32. Springer, New York (2015)
31.
Bérard, B., Haddad, S., Sassolas, M.: Interrupt timed automata: verification and expressiveness. Form. Methods Syst. Des. 40(1), 41–87 (2012)CrossRefMATH
32.
Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP. LNCS, vol. 8169, pp. 1–18. Springer (2013), invited paper
33.
Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Form. Methods Syst. Des. 35(2), 121–151 (2009)CrossRefMATH
34.
Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: complexity and fixed points. In: Hung, D.V., Ogawa, M. (eds.) ATVA. LNCS, vol. 8172, pp. 55–70. Springer, New York (2013)
35.
Brihaye, T., Michaux, C., Rivière, C., Troestler, C.: On O-minimal hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC. LNCS, vol. 2993, pp. 219–233. Springer, New York (2004)
36.
Bruyère, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Log. Methods Comput. Sci. 3(1:7), 1–30 (2007)
37.
Bundala, D., Ouaknine, J.: Advances in parametric real-time reasoning. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS. LNCS, vol. 8634, pp. 123–134. Springer, New York (2014)
38.
Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR. LNCS, vol. 1877, pp. 138–152. Springer, New York (2000)
39.
Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. J. Syst. Softw. 79(10), 1456–1468 (2006)CrossRefMATH
40.
Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Form. Methods Syst. Des. 34(1), 59–81 (2009)CrossRefMATH
41.
Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric metric interval temporal logic. Theor. Comput. Sci. 564, 131–148 (2015)MathSciNetCrossRefMATH
42.
43.
Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: International Computer Music Conference (2013)
44.
Fribourg, L., Lesens, D., Moro, P., Soulat, R.: Robustness analysis for scheduling problems using the inverse method. TIME, pp. 73–80. IEEE Computer Society Press, Silver Spring (2012)
45.
van Glabbeek, R.J.: The linear time-branching time spectrum (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR. LNCS, vol. 458, pp. 278–297. Springer, New York (1990)
46.
Henzinger, T.A.: The theory of hybrid automata. In: Vardi, M.Y., Clarke, E.M. (eds.) LICS. pp. 278–292. IEEE Computer Society, Silver Spring (1996)
47.
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 110–122 (1997)CrossRefMATH
48.
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)MathSciNetCrossRefMATH
49.
Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: Fülöp, Z., Gécseg, F. (eds.) ICALP. LNCS, vol. 944, pp. 417–428. Springer, New York (1995)
50.
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)MathSciNetCrossRefMATH
51.
52.
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52–53, 183–220 (2002)MathSciNetMATH
53.
Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)CrossRefMATH
54.
Jovanović, A.: Parametric verification of timed systems. Ph.D. thesis, École Centrale Nantes, France (2013)
55.
Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. ToPNoC 5, 141–159 (2012)MATH
56.
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef
57.
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)CrossRefMATH
58.
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. LNCS, vol. 5505, pp. 54–57. Springer, New York (2009)
59.
Markey, N.: Robustness in real-time systems. In: Bate, I., Passerone, R. (eds.) SIES, pp. 28–34. IEEE Computer Society Press (2011)
60.
Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, University of California, Irvine, CA, USA (1974)
61.
Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC. LNCS, vol. 1790, pp. 296–309. Springer, New York (2000)
62.
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc, Englewood Cliffs, NJ (1967)MATH
63.
Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Methods Comput. Sci. 3(1), 1–27 (2007)
64.
Ouaknine, J., Worrell, J.: Towards a theory of time-bounded verification. In: Abramsky, S., Gavoille, C., Kirchner, C., auf der Heide, F.M., Spirakis, P.G. (eds.) ICALP Part II. Lecture Notes in Computer Science, vol. 6199, pp. 22–37. Springer, New York (2010)
65.
Quaas, K.: MTL-model checking of one-clock parametric timed automata is undecidable. In: André, É., Frehse, G. (eds.) SynCoP. EPTCS, vol. 145, pp. 5–17 Open Publishing Association, Waterloo, Australia (2014)
66.
Srba, J.: Comparing the expressiveness of timed automata and timed extensions of Petri nets. In: Cassez, F., Jard, C. (eds.) FORMATS. LNCS, vol. 5215, pp. 15–32. Springer, New York (2008)
67.
Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., André, É.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 1–29 (2013)CrossRef
68.
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 709–714. Springer, New York (2009)
69.
Traonouez, L.M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univers. Comput. Sci. 15(17), 3273–3304 (2009)MathSciNetMATH
Metadaten
Titel
What’s decidable about parametric timed automata?
verfasst von
Étienne André
Publikationsdatum
29.07.2017
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2019
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-017-0467-0

Weitere Artikel der Ausgabe 2/2019

International Journal on Software Tools for Technology Transfer 2/2019 Zur Ausgabe

Regular Paper

Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B

Regular Paper

Formal specification and implementation of an automated pattern-based parallel-code generation framework

Regular Paper

A qualitative assessment of Rby in the perspective of the supervisory control theory

Regular Paper

Knowledge-based security testing of web applications by logic programming

Regular Paper

From high-level modeling toward efficient and trustworthy circuits