{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:54Z","timestamp":1750220574041,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_3","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"35-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Parametric Model Checking Timed Automata Under Non-Zenoness Assumption"],"prefix":"10.1007","author":[{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang Gia","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"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."},{"key":"3_CR2","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"},{"key":"3_CR3","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-29510-7_3","volume-title":"Formal Techniques for Safety-Critical Systems","author":"\u00c9 Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9.: What\u2019s decidable about parametric timed automata? In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 52\u201368. Springer, Cham (2016). doi: 10.1007\/978-3-319-29510-7_3"},{"issue":"5","key":"3_CR4","first-page":"819","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819\u2013836 (2009)","journal-title":"IJFCS"},{"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). doi: 10.1007\/978-3-642-32759-9_6"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-47846-3_25","volume-title":"Formal Methods and Software Engineering","author":"\u00c9 Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9., Lime, D., Roux, O.H.: Decision problems for parametric timed automata. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 400\u2013416. Springer, Cham (2016). doi: 10.1007\/978-3-319-47846-3_25"},{"issue":"5\u20136","key":"3_CR7","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/s11241-014-9208-6","volume":"50","author":"\u00c9 Andr\u00e9","year":"2014","unstructured":"Andr\u00e9, \u00c9., Liu, Y., Sun, J., Dong, J.S.: Parameter synthesis for hierarchical concurrent real-time systems. Real-Time Syst. 50(5\u20136), 620\u2013679 (2014)","journal-title":"Real-Time Syst."},{"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, Cham (2015). doi: 10.1007\/978-3-319-22975-1_3"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-319-48989-6_4","volume-title":"FM 2016: Formal Methods","author":"L A\u015ftef\u0103noaei","year":"2016","unstructured":"A\u015ftef\u0103noaei, L., Bensalem, S., Bozga, M., Cheng, C.-H., Ruess, H.: Compositional parameter synthesis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 60\u201368. Springer, Cham (2016). doi: 10.1007\/978-3-319-48989-6_4"},{"issue":"1\u20132","key":"3_CR10","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, 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\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"3_CR11","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00165-006-0010-7","volume":"18","author":"H Bowman","year":"2006","unstructured":"Bowman, H., G\u00f3mez, R.: How to stop time stopping. Formal Aspects Comput. 18(4), 459\u2013493 (2006)","journal-title":"Formal Aspects Comput."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165\u2013168. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679406"},{"issue":"6","key":"3_CR13","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"JS Dong","year":"2008","unstructured":"Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Softw. Eng. 34(6), 844\u2013859 (2008)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-33386-6_22","volume-title":"Automated Technology for Verification and Analysis","author":"S Evangelista","year":"2012","unstructured":"Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 269\u2013283. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33386-6_22"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-75454-1_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R G\u00f3mez","year":"2007","unstructured":"G\u00f3mez, R., Bowman, H.: Efficient detection of Zeno runs in timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 195\u2013210. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75454-1_15"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/s10703-011-0133-1","volume":"40","author":"F Herbreteau","year":"2012","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient emptiness check for timed B\u00fcchi automata. Formal Methods Syst. Des. 40(2), 122\u2013146 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR17","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_CR18","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. Trans. Softw. Eng. 41(5), 445\u2013461 (2015)","journal-title":"Trans. Softw. Eng."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Khatib, L., Muscettola, N., Havelund, K.: Mapping temporal planning constraints into timed automata. In: TIME, pp. 21\u201327. IEEE Computer Society (2001)","DOI":"10.1109\/TIME.2001.930693"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-29072-5_6","volume":"5","author":"M Knapik","year":"2012","unstructured":"Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Models Concurr. 5, 141\u2013159 (2012)","journal-title":"Trans. Petri Nets Models Concurr."},{"issue":"1\u20132","key":"3_CR21","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. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. STTT"},{"key":"3_CR22","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Upper Saddle River (1967)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-25141-7_2","volume-title":"Cyber Physical Systems. Design, Modeling, and Evaluation","author":"S Schupp","year":"2015","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Chen, X., Makhlouf, I.B., Frehse, G., Sankaranarayanan, S., Kowalewski, S.: Current challenges in the verification of hybrid systems. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 8\u201324. Springer, Cham (2015). doi: 10.1007\/978-3-319-25141-7_2"},{"key":"3_CR24","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). doi: 10.1007\/978-3-642-02658-4_59"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 299\u2013314. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48778-6_18"},{"issue":"3","key":"3_CR26","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"S Tripakis","year":"2005","unstructured":"Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed B\u00fcchi automata emptiness efficiently. Formal Methods Syst. Des. 26(3), 267\u2013292 (2005)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"3_CR27","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":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:30:16Z","timestamp":1750195816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"9 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 May 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ti.arc.nasa.gov\/events\/nfm-2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}