{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:35:58Z","timestamp":1784241358046,"version":"3.55.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T00:00:00Z","timestamp":1713312000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T00:00:00Z","timestamp":1713312000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-19-CE25-0015"],"award-info":[{"award-number":["ANR-19-CE25-0015"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s11334-024-00554-5","type":"journal-article","created":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T13:02:03Z","timestamp":1713358923000},"page":"707-726","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Zone extrapolations in parametric timed automata"],"prefix":"10.1007","volume":"21","author":[{"given":"Johan","family":"Arcile","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,4,17]]},"reference":[{"issue":"2","key":"554_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 DL (1994) A theory of timed automata. Theoret Comput Sci 126(2):183\u2013235. https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoret Comput Sci"},{"key":"554_CR2","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1145\/167088.167242","volume-title":"STOC","author":"R Alur","year":"1993","unstructured":"Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: Kosaraju SR, Johnson DS, Aggarwal A (eds) STOC. ACM, New York, pp 592\u2013601. https:\/\/doi.org\/10.1145\/167088.167242"},{"issue":"2","key":"554_CR3","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10009-017-0467-0","volume":"21","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9 \u00c9 (2019) What\u2019s decidable about parametric timed automata? Int J Softw Tools Technol Transf 21(2):203\u2013219. https:\/\/doi.org\/10.1007\/s10009-017-0467-0","journal-title":"Int J Softw Tools Technol Transf"},{"key":"554_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-81685-8_26","volume-title":"CAV","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9 \u00c9 (2021) IMITATOR 3: synthesis of timing parameters beyond decidability. In: Leino R, Silva A (eds) CAV, vol 12759. Lecture Notes in Computer Science. Springer, New York, pp 1\u201314. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_26"},{"key":"554_CR5","doi-asserted-by":"publisher","unstructured":"Andr\u00e9 \u00c9, Lime D (2017) Liveness in L\/U-parametric timed automata. In: Legay A, Schneider K (eds) ACSD. IEEE, pp 9\u201318, https:\/\/doi.org\/10.1109\/ACSD.2017.19","DOI":"10.1109\/ACSD.2017.19"},{"key":"554_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-24288-5_5","volume-title":"RP","author":"\u00c9 Andr\u00e9","year":"2011","unstructured":"Andr\u00e9 \u00c9, Soulat R (2011) Synthesis of timing parameters satisfying safety properties. In: Delzanno G, Potapov I (eds) RP, vol 6945. Lecture Notes in Computer Science. Springer, New York, pp 31\u201344. https:\/\/doi.org\/10.1007\/978-3-642-24288-5_5"},{"issue":"5","key":"554_CR7","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9 \u00c9, Chatain T, Encrenaz E et al (2009) An inverse method for parametric timed automata. Int J Found Comput Sci 20(5):819\u2013836. https:\/\/doi.org\/10.1142\/S0129054109006905","journal-title":"Int J Found Comput Sci"},{"key":"554_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-319-02444-8_27","volume-title":"ATVA","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9 \u00c9, Fribourg L, Soulat R (2013) Merge and conquer: state merging in parametric timed automata. In: Hung DV, Ogawa M (eds) ATVA, vol 8172. Lecture Notes in Computer Science. Springer, New York, pp 381\u2013396. https:\/\/doi.org\/10.1007\/978-3-319-02444-8_27"},{"key":"554_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-319-24537-9","volume-title":"RP","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9 \u00c9, Lime D, Roux OH (2015) Integer-complete synthesis for bounded parametric timed automata. In: Boja\u0144czyk M, Lasota S, Potapov I (eds) RP, vol 9328. LNCS. Springer, New York, pp 7\u201319. https:\/\/doi.org\/10.1007\/978-3-319-24537-9"},{"key":"554_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-00151-3_3","volume-title":"FORMATS","author":"\u00c9 Andr\u00e9","year":"2018","unstructured":"Andr\u00e9 \u00c9, Lime D, Ramparison M (2018) TCTL model checking lower\/upper-bound parametric timed automata without invariants. In: Jansen DN, Prabhakar P (eds) FORMATS, vol 11022. Lecture Notes in Computer Science. Springer, New York, pp 1\u201317. https:\/\/doi.org\/10.1007\/978-3-030-00151-3_3"},{"issue":"1","key":"554_CR11","doi-asserted-by":"publisher","first-page":"15","DOI":"10.23638\/LMCS-16(1:5)2020","volume":"16","author":"\u00c9 Andr\u00e9","year":"2020","unstructured":"Andr\u00e9 \u00c9, Lime D, Markey N (2020) Language preservation problems in parametric timed automata. Log Methods Comput Sci 16(1):15. https:\/\/doi.org\/10.23638\/LMCS-16(1:5)2020","journal-title":"Log Methods Comput Sci"},{"key":"554_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-030-72016-2_17","volume-title":"TACAS","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9 \u00c9, Arias J, Petrucci L et al (2021) Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In: Groote JF, Larsen KG (eds) TACAS, vol 12651. Lecture Notes in Computer Science. Springer, New York, pp 311\u2013329. https:\/\/doi.org\/10.1007\/978-3-030-72016-2_17"},{"issue":"2","key":"554_CR13","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.23638\/LMCS-17(2:13)2021","volume":"17","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9 \u00c9, Lime D, Ramparison M (2021) Parametric updates in parametric timed automata. Log Methods Comput Sci 17(2):13:1-13:67. https:\/\/doi.org\/10.23638\/LMCS-17(2:13)2021","journal-title":"Log Methods Comput Sci"},{"key":"554_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-030-79379-1_3","volume-title":"TAP","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9 \u00c9, Marinho D, van de Pol J (2021) A benchmarks library for extended timed automata. In: Loulergue F, Wotawa F (eds) TAP, vol 12740. Lecture Notes in Computer Science. Springer, New York, pp 39\u201350. https:\/\/doi.org\/10.1007\/978-3-030-79379-1_3"},{"key":"554_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-15839-1_12","volume-title":"FORMATS","author":"\u00c9 Andr\u00e9","year":"2022","unstructured":"Andr\u00e9 \u00c9, Marinho D, Petrucci L et al (2022) Efficient convex zone merging in parametric timed automata. In: Bogomolov S, Parker D (eds) FORMATS, vol 13465. Lecture Notes in Computer Science. Springer, New York, pp 1\u201319. https:\/\/doi.org\/10.1007\/978-3-031-15839-1_12"},{"key":"554_CR16","unstructured":"Andr\u00e9 \u00c9, Lime D, Roux OH (2023) Dense integer-complete synthesis for bounded parametric timed automata. arXiv:2310.09109v1"},{"key":"554_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-031-06773-0_24","volume-title":"NFM","author":"J Arcile","year":"2022","unstructured":"Arcile J, Andr\u00e9 \u00c9 (2022) Zone extrapolations in parametric timed automata. In: Deshmukh JV, Havelund K, Perez I (eds) NFM, vol 13260. Lecture Notes in Computer Science. Springer, New York, pp 451\u2013469. https:\/\/doi.org\/10.1007\/978-3-031-06773-0_24"},{"issue":"1\u20132","key":"554_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara R, Hill PM, Zaffanella E (2008) 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\u20132):3\u201321. https:\/\/doi.org\/10.1016\/j.scico.2007.08.001","journal-title":"Sci Comput Program"},{"key":"554_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-36577-X_18","volume-title":"TACAS","author":"G Behrmann","year":"2003","unstructured":"Behrmann G, Bouyer P, Fleury E et al (2003) Static guard analysis in timed automata verification. In: Garavel H, Hatcliff J (eds) TACAS, vol 2619. Lecture Notes in Computer Science. Springer, New York, pp 254\u2013277. https:\/\/doi.org\/10.1007\/3-540-36577-X_18"},{"issue":"3","key":"554_CR20","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2006","unstructured":"Behrmann G, Bouyer P, Larsen KG et al (2006) Lower and upper bounds in zone-based abstractions of timed automata. Int J Softw Tools Technol Transf 8(3):204\u2013215. https:\/\/doi.org\/10.1007\/s10009-005-0190-0","journal-title":"Int J Softw Tools Technol Transf"},{"key":"554_CR21","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":"ICALP, Part II","author":"N Bene\u0161","year":"2015","unstructured":"Bene\u0161 N, Bezd\u011bk P, Larsen KG et al (2015) Language emptiness of continuous-time parametric timed automata. In: Halld\u00f3rsson MM, Iwama K, Kobayashi N et al (eds) ICALP, Part II, vol 9135. Lecture Notes in Computer Science. Springer, New York, pp 69\u201381. https:\/\/doi.org\/10.1007\/978-3-662-47666-6_6"},{"key":"554_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-41591-8_12","volume-title":"SEFM","author":"P Bezd\u011bk","year":"2016","unstructured":"Bezd\u011bk P, Bene\u0161 N, Barnat J et al (2016) LTL parameter synthesis of parametric timed automata. In: Nicola RD, K\u00fchn E (eds) SEFM, vol 9763. Lecture Notes in Computer Science. Springer, New York, pp 172\u2013187. https:\/\/doi.org\/10.1007\/978-3-319-41591-8_12"},{"issue":"2","key":"554_CR23","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 (2009) Decision problems for lower\/upper bound parametric timed automata. Form Methods Syst Des 35(2):121\u2013151. https:\/\/doi.org\/10.1007\/s10703-009-0074-0","journal-title":"Form Methods Syst Des"},{"key":"554_CR24","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.ic.2016.07.011","volume":"253","author":"D Bundala","year":"2017","unstructured":"Bundala D, Ouaknine J (2017) On parametric timed automata and one-counter machines. Inf Comput 253:272\u2013303. https:\/\/doi.org\/10.1016\/j.ic.2016.07.011","journal-title":"Inf Comput"},{"key":"554_CR25","doi-asserted-by":"publisher","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Steffen B (ed) TACAS, vol 1384. Lecture Notes in Computer Science. Springer, New York, pp 313\u2013329. https:\/\/doi.org\/10.1007\/BFb0054180","DOI":"10.1007\/BFb0054180"},{"key":"554_CR26","doi-asserted-by":"publisher","unstructured":"G\u00f6ller S, Hilaire M (2021) Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete. In: Bl\u00e4ser M, Monmege B (eds) STACS, LIPIcs, vol 187. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp 36:1\u201336:18. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2021.36","DOI":"10.4230\/LIPIcs.STACS.2021.36"},{"key":"554_CR27","doi-asserted-by":"publisher","unstructured":"Herbreteau F, Kini D, Srivathsan B, et\u00a0al (2011) Using non-convex approximations for efficient analysis of timed automata. In: Chakraborty S, Kumar A (eds) FSTTCS, LIPIcs, vol\u00a013. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp 78\u201389. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2011.78","DOI":"10.4230\/LIPIcs.FSTTCS.2011.78"},{"key":"554_CR28","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.ic.2016.07.004","volume":"251","author":"F Herbreteau","year":"2016","unstructured":"Herbreteau F, Srivathsan B, Walukiewicz I (2016) Better abstractions for timed automata. Inf Comput 251:67\u201390. https:\/\/doi.org\/10.1016\/j.ic.2016.07.004","journal-title":"Inf Comput"},{"key":"554_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune T, Romijn J, Stoelinga M et al (2002) Linear parametric model checking of timed automata. J Log Algebr Program 52\u201353:183\u2013220. https:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","journal-title":"J Log Algebr Program"},{"key":"554_CR30","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107 A, Lime D, Roux OH (2015) Integer parameter synthesis for real-time systems. IEEE Trans Softw Eng 41(5):445\u2013461. https:\/\/doi.org\/10.1109\/TSE.2014.2357445","DOI":"10.1109\/TSE.2014.2357445"},{"issue":"1\u20132","key":"554_CR31","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1\u20132):134\u2013152. https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"Int J Softw Tools Technol Transf"},{"key":"554_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-04368-0_18","volume-title":"FORMATS","author":"G Li","year":"2009","unstructured":"Li G (2009) Checking timed B\u00fcchi automata emptiness using LU-abstractions. In: Ouaknine J, Vaandrager FW (eds) FORMATS, vol 5813. Lecture Notes in Computer Science. Springer, New York, pp 228\u2013242. https:\/\/doi.org\/10.1007\/978-3-642-04368-0_18"},{"key":"554_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"HSCC","author":"JS Miller","year":"2000","unstructured":"Miller JS (2000) Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch NA, Krogh BH (eds) HSCC, vol 1790. Lecture Notes in Computer Science. Springer, New York, pp 296\u2013309. https:\/\/doi.org\/10.1007\/3-540-46430-1_26"},{"key":"554_CR34","doi-asserted-by":"publisher","unstructured":"Nguyen HG, Petrucci L, van\u00a0de Pol J (2018) Layered and collecting NDFS with subsumption for parametric timed automata. In: Lin AW, Sun J (eds) ICECCS. IEEE Computer Society, pp 1\u20139, https:\/\/doi.org\/10.1109\/ICECCS2018.2018.00009","DOI":"10.1109\/ICECCS2018.2018.00009"},{"key":"554_CR35","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"issue":"3","key":"554_CR36","doi-asserted-by":"publisher","first-page":"15:1","DOI":"10.1145\/1507244.1507245","volume":"10","author":"S Tripakis","year":"2009","unstructured":"Tripakis S (2009) Checking timed B\u00fcchi automata emptiness on simulation graphs. ACM Trans Comput Log 10(3):15:1-15:19. https:\/\/doi.org\/10.1145\/1507244.1507245","journal-title":"ACM Trans Comput Log"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00554-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-024-00554-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00554-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:05:22Z","timestamp":1750316722000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-024-00554-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,17]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["554"],"URL":"https:\/\/doi.org\/10.1007\/s11334-024-00554-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,17]]},"assertion":[{"value":"6 December 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to participate"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}}]}}