{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T12:57:22Z","timestamp":1726059442775},"publisher-location":"Berlin, Heidelberg","reference-count":71,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662606506"},{"type":"electronic","value":"9783662606513"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-662-60651-3_3","type":"book-chapter","created":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T01:04:25Z","timestamp":1574211865000},"page":"64-100","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Parametric Verification: An Introduction"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-3259-9786","authenticated-orcid":false,"given":"Micha\u0142","family":"Knapik","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-9429-7586","authenticated-orcid":false,"given":"Didier","family":"Lime","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-6477-4863","authenticated-orcid":false,"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-3154-5268","authenticated-orcid":false,"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-49382-2_22","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"L Aceto","year":"1998","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245\u2013256. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-540-49382-2_22"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1024","journal-title":"Inf. Comput."},{"issue":"2","key":"3_CR3","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). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC, pp. 592\u2013601. ACM, New York (1993). https:\/\/doi.org\/10.1145\/167088.167242","DOI":"10.1145\/167088.167242"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-319-46750-4_27","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"\u00c9 Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9.: Parametric deadlock-freeness checking timed automata. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 469\u2013478. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_27"},{"key":"3_CR6","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-12988-0_5","volume-title":"Formal Techniques for Safety-Critical Systems","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9, \u00c9.: A benchmark library for parametric timed model checking. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 75\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-12988-0_5"},{"issue":"2","key":"3_CR7","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.: What\u2019s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. 21(2), 203\u2013219 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0467-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-030-17465-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9, \u00c9., Bloemen, V., Petrucci, L., van de Pol, J.: Minimal-time synthesis for parametric timed automata. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 211\u2013228. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_12"},{"issue":"5","key":"3_CR9","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., Fribourg, L.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819\u2013836 (2009). https:\/\/doi.org\/10.1142\/S0129054109006905","journal-title":"Int. J. Found. Comput. Sci."},{"key":"3_CR10","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). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_6"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: Lin, A.W., Sun, J. (eds.) ICECCS, pp. 10\u201320. IEEE CPS (2018). https:\/\/doi.org\/10.1109\/ICECCS2018.2018.00010","DOI":"10.1109\/ICECCS2018.2018.00010"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Lime, D.: Liveness in L\/U-parametric timed automata. In: Legay, A., Schneider, K. (eds.) ACSD, pp. 9\u201318. IEEE (2017). https:\/\/doi.org\/10.1109\/ACSD.2017.19","DOI":"10.1109\/ACSD.2017.19"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-030-00151-3_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"\u00c9 Andr\u00e9","year":"2018","unstructured":"Andr\u00e9, \u00c9., Lime, D., Ramparison, M.: TCTL model checking lower\/upper-bound parametric timed automata without invariants. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 37\u201352. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00151-3_3"},{"key":"3_CR14","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). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_25"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-17524-9_5","volume-title":"NASA Formal Methods","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9, \u00c9., Lipari, G., Nguyen, H.G., Sun, Y.: Reachability preservation based parameter synthesis for timed automata. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 50\u201365. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_5"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"984","DOI":"10.1007\/978-3-642-39799-8_70","volume-title":"Computer Aided Verification","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9, \u00c9., 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 2013. LNCS, vol. 8044, pp. 984\u2013989. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_70"},{"key":"3_CR17","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). https:\/\/doi.org\/10.1007\/978-3-319-22975-1_3"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-57288-8_3","volume-title":"NASA Formal Methods","author":"\u00c9 Andr\u00e9","year":"2017","unstructured":"Andr\u00e9, \u00c9., Nguyen, H.G., Petrucci, L., Sun, J.: Parametric model checking timed automata under non-zenoness assumption. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 35\u201351. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_3"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Soulat, R.: The Inverse Method. FOCUS Series in Computer Engineering and Information Technology, ISTE Ltd and Wiley, 176 p. (2013)","DOI":"10.1002\/9781118569351"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.biosystems.2016.09.002","volume":"149","author":"A Andreychenko","year":"2016","unstructured":"Andreychenko, A., Magnin, M., Inoue, K.: Analyzing resilience properties in oscillatory biological systems using parametric model checking. Biosystems 149, 50\u201358 (2016). https:\/\/doi.org\/10.1016\/j.biosystems.2016.09.002 . Selected Papers from the Computational Methods in Systems Biology 2015 Conference","journal-title":"Biosystems"},{"key":"3_CR21","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). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_4"},{"issue":"1\u20132","key":"3_CR22","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). https:\/\/doi.org\/10.1016\/j.scico.2007.08.001","journal-title":"Sci. Comput. Program."},{"key":"3_CR23","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. LNCS, vol. 9135, pp. 69\u201381. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_6"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, 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 2005. LNCS, vol. 3829, pp. 211\u2013225. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_17"},{"key":"3_CR25","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). https:\/\/doi.org\/10.1007\/978-3-642-41036-9_1"},{"issue":"2","key":"3_CR26","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 Methods Syst. Design 35(2), 121\u2013151 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0074-0","journal-title":"Formal Methods Syst. Design"},{"issue":"8","key":"3_CR27","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Trans. Comput."},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. LNCS, vol. 8634, pp. 123\u2013134. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44522-8_11"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{20}$$ states and beyond. In: LICS, pp. 428\u2013439. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"issue":"1","key":"3_CR30","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 Methods Syst. Des. 34(1), 59\u201381 (2009). https:\/\/doi.org\/10.1007\/s10703-008-0061-x","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR31","unstructured":"David, N.: Discrete parameters in Petri nets. Ph.D. thesis. University of Nantes, France (2017)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-19488-2_7","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"N David","year":"2015","unstructured":"David, N., Jard, C., Lime, D., Roux, O.H.: Discrete parameters in Petri nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 137\u2013156. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19488-2_7"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"David, N., Jard, C., Lime, D., Roux, O.H.: Coverability synthesis in parametric Petri nets. In: Meyer, R., Nestmann, U. (eds.) CONCUR. LIPIcs, Dagstuhl Publishing (2017). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.14","DOI":"10.4230\/LIPIcs.CONCUR.2017.14"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Delahaye, B.: Consistency for parametric interval Markov chains. In: Andr\u00e9, \u00c9., Frehse, G. (eds.) SynCoP. OASICS, vol. 44, pp. 17\u201332. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/OASIcs.SynCoP.2015.17","DOI":"10.4230\/OASIcs.SynCoP.2015.17"},{"issue":"3","key":"3_CR35","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.jlap.2011.10.003","volume":"81","author":"B Delahaye","year":"2012","unstructured":"Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Consistency and refinement for interval Markov chains. J. Log. Algebr. Program. 81(3), 209\u2013226 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2011.10.003","journal-title":"J. Log. Algebr. Program."},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-662-49122-5_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Delahaye","year":"2016","unstructured":"Delahaye, B., Lime, D., Petrucci, L.: Parameter synthesis for parametric interval Markov chains. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 372\u2013390. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_18"},{"issue":"5","key":"3_CR37","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1016\/j.jcss.2013.01.014","volume":"79","author":"S Demri","year":"2013","unstructured":"Demri, S.: On selective unboundedness of VASS. J. Comput. Syst. Sci. 79(5), 689\u2013713 (2013). https:\/\/doi.org\/10.1016\/j.jcss.2013.01.014","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.tcs.2014.11.019","volume":"564","author":"B Giampaolo Di","year":"2015","unstructured":"Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric metric interval temporal logic. Theoret. Comput. Sci. 564, 131\u2013148 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2014.11.019","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"3_CR39","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). https:\/\/doi.org\/10.1016\/j.ipl.2006.11.018","journal-title":"Inf. Process. Lett."},{"key":"3_CR40","unstructured":"Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: ICMC. Michigan Publishing, August 2013"},{"issue":"3","key":"3_CR41","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0062-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Fribourg, L., Lesens, D., Moro, P., Soulat, R.: Robustness analysis for scheduling problems using the inverse method. In: Reynolds, M., Terenziani, P., Moszkowski, B. (eds.) TIME, pp. 73\u201380. IEEE Computer Society Press, September 2012. https:\/\/doi.org\/10.1109\/TIME.2012.10 . http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PDF\/FLMS-time12.pdf","DOI":"10.1109\/TIME.2012.10"},{"issue":"1","key":"3_CR44","doi-asserted-by":"crossref","first-page":"29","DOI":"10.3233\/FI-2015-1169","volume":"137","author":"G Geeraerts","year":"2015","unstructured":"Geeraerts, G., Heu\u00dfner, A., Praveen, M., Raskin, J.: $$\\omega $$-Petri nets: algorithms and complexity. Fundamenta Informaticae 137(1), 29\u201360 (2015)","journal-title":"Fundamenta Informaticae"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039066"},{"issue":"1\u20132","key":"3_CR46","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997). https:\/\/doi.org\/10.1007\/s100090050008","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR47","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1985)"},{"key":"3_CR48","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., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52\u201353, 183\u2013220 (2002). https:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","journal-title":"J. Log. Algebr. Program."},{"key":"3_CR49","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)"},{"issue":"5","key":"3_CR50","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 real-time systems. IEEE Trans. Softw. Eng. 41(5), 445\u2013461 (2015). https:\/\/doi.org\/10.1109\/TSE.2014.2357445","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"3_CR51","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969). https:\/\/doi.org\/10.1016\/S0022-0000(69)80011-5","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR52","unstructured":"Knapik, M.: https:\/\/michalknapik.github.io\/spatula"},{"issue":"4","key":"3_CR53","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2746337","volume":"14","author":"M Knapik","year":"2015","unstructured":"Knapik, M., Meski, A., Penczek, W.: Action synthesis for branching time logic: theory and applications. ACM Trans. Embed. Comput. 14(4), 64 (2015). https:\/\/doi.org\/10.1145\/2746337","journal-title":"ACM Trans. Embed. Comput."},{"key":"3_CR54","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 Other Models Concurr. 5, 141\u2013159 (2012). https:\/\/doi.org\/10.1007\/978-3-642-29072-5_6","journal-title":"Trans. Petri Nets Other Models Concurr."},{"key":"3_CR55","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11313-5_22","volume-title":"Intelligent Systems\u20192014","author":"M Knapik","year":"2015","unstructured":"Knapik, M., Penczek, W.: Fixed-point methods in parametric model checking. In: Angelov, P., et al. (eds.) Intelligent Systems\u20192014. AISC, vol. 322, pp. 231\u2013242. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-11313-5_22"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-68690-5_15","volume-title":"Formal Methods and Software Engineering","author":"J Li","year":"2017","unstructured":"Li, J., Sun, J., Gao, B., Andr\u00e9, \u00c9.: Classification-based parameter synthesis for\u00a0parametric timed automata. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 243\u2013261. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_15"},{"key":"3_CR57","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). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6"},{"key":"3_CR58","doi-asserted-by":"publisher","unstructured":"Luthmann, L., Stephan, A., B\u00fcrdek, J., Lochau, M.: Modeling and testing product lines with unbounded parametric real-time constraints. In: Cohen, M.B., et al. (eds.) SPLC, vol. A, pp. 104\u2013113. ACM (2017). https:\/\/doi.org\/10.1145\/3106195.3106204","DOI":"10.1145\/3106195.3106204"},{"key":"3_CR59","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., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296\u2013310. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46430-1_26"},{"volume-title":"Computation: Finite and Infinite Machines","year":"1967","author":"ML Minsky","key":"3_CR60","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Upper Saddle River (1967)"},{"key":"3_CR61","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-53946-1_8","volume-title":"Formal Techniques for Safety-Critical Systems","author":"B Parquier","year":"2017","unstructured":"Parquier, B., et al.: Applying parametric model-checking techniques for reusing real-time critical systems. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 129\u2013144. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-53946-1_8"},{"key":"3_CR62","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS (LNAI), vol. 4428, pp. 113\u2013128. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74128-2_8"},{"key":"3_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-92612-4_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Petrucci","year":"2018","unstructured":"Petrucci, L., van de Pol, J.: Parameter synthesis algorithms for parametric interval Markov chains. In: Baier, C., Caires, L. (eds.) FORTE 2018. LNCS, vol. 10854, pp. 121\u2013140. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92612-4_7"},{"issue":"2","key":"3_CR64","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.jal.2005.12.010","volume":"5","author":"F Raimondi","year":"2007","unstructured":"Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Appl. Log. 5(2), 235\u2013251 (2007). https:\/\/doi.org\/10.1016\/j.jal.2005.12.010","journal-title":"J. Appl. Log."},{"key":"3_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-662-46681-0_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Sankur","year":"2015","unstructured":"Sankur, O.: Symbolic quantitative robustness analysis of timed automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 484\u2013498. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_48"},{"key":"3_CR66","unstructured":"Seidner, C.: V\u00e9rification des EFFBDs: model checking en Ing\u00e9nierie Syst\u00e8me. (EFFBDs verification: model checking in systems engineering). Ph.D. thesis. University of Nantes, France (2009). https:\/\/tel.archives-ouvertes.fr\/tel-00440677"},{"key":"3_CR67","unstructured":"Somenzi, F.: CUDD: CU decision diagram package - release 2.5.0. https:\/\/github.com\/ivmai\/cudd"},{"issue":"1","key":"3_CR68","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2430536.2430537","volume":"22","author":"J Sun","year":"2013","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, \u00c9.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 3:1\u20133:29 (2013). https:\/\/doi.org\/10.1145\/2430536.2430537","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"3_CR69","unstructured":"Sun, Y., Andr\u00e9, \u00c9., Lipari, G.: Verification of two real-time systems using parametric timed automata. In: Quinton, S., Vardanega, T. (eds.) WATERS, July 2015"},{"issue":"17","key":"3_CR70","doi-asserted-by":"publisher","first-page":"3273","DOI":"10.3217\/jucs-015-17-3273","volume":"15","author":"LM Traonouez","year":"2009","unstructured":"Traonouez, L.M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univ. Comput. Sci. 15(17), 3273\u20133304 (2009). https:\/\/doi.org\/10.3217\/jucs-015-17-3273","journal-title":"J. Univ. Comput. Sci."},{"issue":"6","key":"3_CR71","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/BF00289715","volume":"21","author":"R Valk","year":"1985","unstructured":"Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica 21(6), 643\u2013674 (1985). https:\/\/doi.org\/10.1007\/BF00289715","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XIV"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-60651-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,12]],"date-time":"2019-12-12T13:43:49Z","timestamp":1576158229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-60651-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783662606506","9783662606513"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-60651-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}
