{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:47:31Z","timestamp":1742914051678,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912677"},{"type":"electronic","value":"9783319912684"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-91268-4_1","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T16:27:38Z","timestamp":1525710458000},"page":"3-15","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Self-adaptive Model Checking, the Next Step?"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Kordon","sequence":"first","affiliation":[]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-662-48899-7_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Souheib Baarir","year":"2015","unstructured":"Baarir, S., Duret-Lutz, A.: Sat-based minimization of deterministic $$\\omega $$-automata. In: 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, pp. 79\u201387 (2015)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-54862-8_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AE Ben Salem","year":"2014","unstructured":"Ben Salem, A.E., Duret-Lutz, A., Kordon, F., Thierry-Mieg, Y.: Symbolic model checking of stutter-invariant properties using generalized testing automata. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 440\u2013454. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_38"},{"key":"1_CR3","unstructured":"Berthomieux, B., Bodeveix, J.P., Filali, M., Lang, F., Le Botland, D., Vernadat, F.: The syntax and semantic of fiacre. Technical report 7264, CNRS-LAAS (2007)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","author":"R Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 222\u2013235. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_21"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b137241","volume-title":"Model-Based Testing of Reactive Systems","year":"2005","unstructured":"Broy, M., Jonsson, B., Katoen, J., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/b137241"},{"key":"1_CR6","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Congress on Logic, Method, and Philosophy of Science, pp. 1\u201312. Stanford University (1960, 1962)"},{"issue":"2","key":"1_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{\\hat{}}$$20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"11","key":"1_CR8","doi-asserted-by":"publisher","first-page":"1343","DOI":"10.1109\/12.247838","volume":"42","author":"G Chiola","year":"1993","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Comput. 42(11), 1343\u20131360 (1993)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"1_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583\u2013604 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10009-002-0103-4","volume":"4","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Jha, S., Marrero, W.R.: Efficient verification of security protocols using partial-order reductions. STTT 4(2), 173\u2013188 (2003)","journal-title":"STTT"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"830","DOI":"10.1007\/978-3-642-39799-8_58","volume-title":"Computer Aided Verification","author":"M Colange","year":"2013","unstructured":"Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Towards distributed software model-checking using decision diagrams. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 830\u2013845. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_58"},{"issue":"6","key":"1_CR12","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A formal analysis of bluetooth device discovery. STTT 8(6), 621\u2013632 (2006)","journal-title":"STTT"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-24372-1_24","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2011","unstructured":"Duret-Lutz, A., Klai, K., Poitrenaud, D., Thierry-Mieg, Y.: Self-loop aggregation product\u2014a new hybrid approach to on-the-fly LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 336\u2013350. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_24"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/11562948_17","volume-title":"Automated Technology for Verification and Analysis","author":"S. Evangelista","year":"2005","unstructured":"Evangelista, S., Haddad, S., Pradat-Peyre, J.: Syntactical colored petri nets reductions. In: Automated Technology for Verification and Analysis, Third International Symposium, ATVA. pp. 202\u2013216 (2005)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-19488-2_9","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"H Garavel","year":"2015","unstructured":"Garavel, H.: Nested-unit petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 179\u2013199. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19488-2_9"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/11691617_4","volume-title":"Model Checking Software","author":"J Geldenhuys","year":"2006","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53\u201370. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_4"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/3-540-45139-0_2","volume-title":"Model Checking Software","author":"R Gerth","year":"2001","unstructured":"Gerth, R.: Model checking if your life depends on it: a view from intel\u2019s trenches. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, p. 15. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45139-0_2"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Groce","year":"2002","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357\u2013370. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_25"},{"issue":"3\u20134","key":"1_CR20","first-page":"413","volume":"94","author":"A Hamez","year":"2009","unstructured":"Hamez, A., Thierry-Mieg, Y., Kordon, F.: Building efficient model checkers using hierarchical set decision diagrams and automatic saturation. Fundam. Inf. 94(3\u20134), 413\u2013437 (2009)","journal-title":"Fundam. Inf."},{"key":"1_CR21","unstructured":"Hillah, L., Kindler, E., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: A primer on the Petri Net Markup Language and ISO\/IEC 15909\u20132. In: Petri Net Newsletter (originally presented at the 10th International workshop on Practical Use of Colored Petri Nets and the CPN Tools - CPN 2009), vol. 76, pp. 9\u201328 (2009)"},{"key":"1_CR22","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)","edition":"1"},{"issue":"2","key":"1_CR23","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2004.08.062","volume":"133","author":"J\u00e9r\u00f4me Hugues","year":"2005","unstructured":"Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Baarir, S., Vergnaud, T.: On the formal verification of middleware behavioral properties. In: 9th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004), pp. 139\u2013157. Elsevier (2004)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-68746-7_20","volume-title":"Applications and Theory of Petri Nets","author":"K Klai","year":"2008","unstructured":"Klai, K., Poitrenaud, D.: MC-SOG: an LTL model checker based on symbolic observation graphs. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 288\u2013306. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68746-7_20"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Kordon, F., Leuschel, M., van de Pol, J., Thierry-Mieg, Y.: Software architecture of modern model checkers. In: High Assurance System: Methods, Languages, and Tools. LNCS 10000 (2018, to appear)","DOI":"10.1007\/978-3-319-91908-9_20"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-662-53401-4_12","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"F Kordon","year":"2016","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Paviot-Adet, E., Jezequel, L., Rodr\u00edguez, C., Hulin-Hubard, F.: MCC\u20192015 \u2013 the fifth model checking contest. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 262\u2013273. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_12"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164\u2013177. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_14"},{"key":"1_CR30","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. AMS 141, 1\u201335 (1969)","journal-title":"Trans. AMS"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1007\/978-3-642-36742-7_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Renault","year":"2013","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Strength-based decomposition of the property B\u00fcchi automaton for faster model checking. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 580\u2013593. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_42"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-44919-1_29","volume-title":"Applications and Theory of Petri Nets 2003","author":"C Schr\u00f6ter","year":"2003","unstructured":"Schr\u00f6ter, C., Schwoon, S., Esparza, J.: The model-checking kit. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 463\u2013472. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44919-1_29"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-03845-7_20","volume-title":"Computational Methods in Systems Biology","author":"M Schwarick","year":"2009","unstructured":"Schwarick, M., Heiner, M.: CSL model checking of biochemical networks with interval decision diagrams. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 296\u2013312. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03845-7_20"},{"issue":"1\/2","key":"1_CR34","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"RS Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54(1\/2), 121\u2013141 (1982)","journal-title":"Inf. Control"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"},{"issue":"6","key":"1_CR36","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/TSE.2004.15","volume":"30","author":"F Wang","year":"2004","unstructured":"Wang, F., Schmidt, K., Yu, F., Huang, G., Wang, B.: BDD-based safety-analysis of concurrent software with pointer data structures using graph automorphism symmetry reduction. IEEE Trans. Softw. Eng. 30(6), 403\u2013417 (2004)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91268-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:21:35Z","timestamp":1710267695000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-91268-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912677","9783319912684"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91268-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"8 May 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bratislava","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Slovakia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 June 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 June 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"39","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/interes.institute\/petrinets2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}