{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:37:14Z","timestamp":1743014234681,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319295091"},{"type":"electronic","value":"9783319295107"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29510-7_3","type":"book-chapter","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T09:39:16Z","timestamp":1454060356000},"page":"52-68","source":"Crossref","is-referenced-by-count":11,"title":["What\u2019s Decidable About Parametric Timed Automata?"],"prefix":"10.1007","author":[{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"3_CR2","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R Alur","year":"2001","unstructured":"Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for \u201cmodel measuring\u201d. ACM Trans. Comput. Logic 2(3), 388\u2013407 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"issue":"05","key":"3_CR4","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9TIENNE ANDR\u00c9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, Th., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819\u2013836 (2009)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9 Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33\u201336. Springer, Heidelberg (2012)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-319-24537-9_2","volume-title":"Reachability Problems","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9, \u00c9., 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\u201319. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-319-24537-9_2"},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/978-3-319-47846-3_25","volume-title":"Formal Methods and Software Engineering","author":"\u00c9tienne Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9., Lime, D., Roux, O.H.: Decision problems for parametric timed automata (submitted, 2016)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-22975-1_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9, \u00c9., Markey, N.: Language preservation problems in parametric timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 27\u201343. Springer, Heidelberg (2015)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1016\/j.ic.2011.11.006","volume":"211","author":"E Asarin","year":"2012","unstructured":"Asarin, E., Mysore, V., Pnueli, A., Schneider, G.: Low dimensional hybrid systems \u2013 decidable, undecidable, don\u2019t know. Inf. Comput. 211, 138\u2013159 (2012)","journal-title":"Inf. Comput."},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-662-47666-6_6","volume-title":"Automata, Languages, and Programming","author":"N Bene\u0161","year":"2015","unstructured":"Bene\u0161, N., Bezd\u011bk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015, Part II. LNCS, vol. 9135, pp. 69\u201381. Springer, Heidelberg (2015)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-41036-9_7","volume-title":"Reachability Problems","author":"B B\u00e9rard","year":"2013","unstructured":"B\u00e9rard, B., Haddad, S., Jovanovi\u0107, A., Lime, D.: Parametric interrupt timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 59\u201369. Springer, Heidelberg (2013)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-41036-9_1","volume-title":"Reachability Problems","author":"P Bouyer","year":"2013","unstructured":"Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 1\u201318. Springer, Heidelberg (2013)"},{"issue":"2","key":"3_CR13","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10703-009-0074-0","volume":"35","author":"L Bozzelli","year":"2009","unstructured":"Bozzelli, L., La Torre, S.: Decision problems for lower\/upper bound parametric timed automata. Formal Meth. Syst. Des. 35(2), 121\u2013151 (2009)","journal-title":"Formal Meth. Syst. Des."},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-02444-8_6","volume-title":"Automated Technology for Verification and Analysis","author":"T Brihaye","year":"2013","unstructured":"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\u201370. Springer, Heidelberg (2013)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Bruy\u00e8re, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Logical Meth. Comput. Sci. 3(1: 7), 1\u201330 (2007)","DOI":"10.2168\/LMCS-3(1:7)2007"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-662-44522-8_11","volume-title":"Mathematical Foundations of Computer Science 2014","author":"D Bundala","year":"2014","unstructured":"Bundala, D., Ouaknine, J.: Advances in parametric real-time reasoning. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 123\u2013134. Springer, Heidelberg (2014)"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10703-008-0061-x","volume":"34","author":"R Chevallier","year":"2009","unstructured":"Chevallier, R., Encrenaz-Tiph\u00e8ne, 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\u201381 (2009)","journal-title":"Formal Meth. Syst. Des."},{"issue":"5","key":"3_CR18","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/j.ipl.2006.11.018","volume":"102","author":"L Doyen","year":"2007","unstructured":"Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208\u2013213 (2007)","journal-title":"Inf. Process. Lett."},{"key":"3_CR19","unstructured":"Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: International Computer Music Conference (2013)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Lesens, D., Moro, P., Soulat, R.: Robustness analysis for scheduling problems using the inverse method. In: TIME, pp. 73\u201380. IEEE Computer Society Press (2012)","DOI":"10.1109\/TIME.2012.10"},{"issue":"1","key":"3_CR21","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/3-540-60084-1_93","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: F\u00fcl\u00f6p, Z. (ed.) ICALP 1995. LNCS, vol. 944, pp. 417\u2013428. Springer, Heidelberg (1995)"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"3_CR24","first-page":"183","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52\u201353, 183\u2013220 (2002)","journal-title":"JLAP"},{"issue":"5","key":"3_CR25","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1109\/TSE.2014.2357445","volume":"41","author":"A Jovanovi\u0107","year":"2015","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445\u2013461 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR26","unstructured":"Jovanovi\u0107, A.: Parametric verification of timed systems. Ph.D. thesis , \u00c9cole Centrale Nantes, France (2013)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-29072-5_6","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"M Knapik","year":"2012","unstructured":"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\u2013159. Springer, Heidelberg (2012)"},{"issue":"1\u20132","key":"3_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"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\u201357. Springer, Heidelberg (2009)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"Hybrid Systems: Computation and Control","author":"JS Miller","year":"2000","unstructured":"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)"},{"key":"3_CR31","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Englewood Cliffs (1967)"},{"key":"3_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.4204\/EPTCS.145.3","volume":"145","author":"K Quaas","year":"2014","unstructured":"Quaas, K.: MTL-model checking of one-clock parametric timed automata is undecidable. SynCoP. EPTCS 145, 5\u201317 (2014)","journal-title":"SynCoP. EPTCS"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"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\u2013714. Springer, Heidelberg (2009)"},{"issue":"1","key":"3_CR34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TSE.2014.2359893","volume":"41","author":"T Wang","year":"2015","unstructured":"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\u201318 (2015)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29510-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T08:19:49Z","timestamp":1559377189000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29510-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319295091","9783319295107"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29510-7_3","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]}}}