×

zbMATH — the first resource for mathematics

What’s decidable about parametric timed automata? (English) Zbl 1396.68064
Artho, Cyrille (ed.) et al., Formal techniques for safety-critical systems. Fourth international workshop, FTSCS 2015, Paris, France, November 6–7, 2015. Revised selected papers. Cham: Springer (ISBN 978-3-319-29509-1/pbk; 978-3-319-29510-7/ebook). Communications in Computer and Information Science 596, 52-68 (2016).
Summary: 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.
For the entire collection see [Zbl 1393.68009].

MSC:
68Q45 Formal languages and automata
Software:
IMITATOR; PAT; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1.Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183-235 (1994) · Zbl 0803.68071
[2] 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) · Zbl 1171.68544
[3] 3.Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592-601. ACM (1993) · Zbl 1310.68139
[4] 4.André, É., Chatain, Th., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819-836 (2009) · Zbl 1187.68286
[5] 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)
[6] 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: · Zbl 06798762
[7] 7.André, É., Lime, D., Roux, O.H.: Decision problems for parametric timed automata (submitted, 2016)
[8] 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) · Zbl 06481820
[9] 9.Asarin, E., Mysore, V., Pnueli, A., Schneider, G.: Low dimensional hybrid systems - decidable, undecidable, don’t know. Inf. Comput. 211, 138-159 (2012) · Zbl 1279.68127
[10] 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) · Zbl 1440.68150
[11] 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) · Zbl 1355.68148
[12] 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) · Zbl 1407.68282
[13] 13.Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Meth. Syst. Des. 35(2), 121-151 (2009) · Zbl 1186.68245
[14] 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) · Zbl 1410.68198
[15] 15.Bruyère, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Logical Meth. Comput. Sci. 3(1: 7), 1-30 (2007) · Zbl 1128.68052
[16] 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) · Zbl 1426.68140
[17] 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) · Zbl 1165.68401
[18] 18.Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208-213 (2007) · Zbl 1184.68337
[19] 19.Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: International Computer Music Conference (2013)
[20] 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)
[21] 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) · Zbl 0920.68091
[22] 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)
[23] 23.Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193-244 (1994) · Zbl 0806.68080
[24] 24.Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52-53, 183-220 (2002) · Zbl 1008.68069
[25] 25.Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445-461 (2015) · Zbl 1381.68121
[26] 26.Jovanović, A.: Parametric verification of timed systems. Ph.D. thesis , École Centrale Nantes, France (2013)
[27] 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) · Zbl 1350.68183
[28] 28.Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1-2), 134-152 (1997) · Zbl 1060.68577
[29] 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)
[30] 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) · Zbl 0992.93050
[31] 31.Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Englewood Cliffs (1967) · Zbl 0195.02402
[32] 32.Quaas, K.: MTL-model checking of one-clock parametric timed automata is undecidable. SynCoP. EPTCS 145, 5-17 (2014)
[33] 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)
[34] 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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.