{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:30Z","timestamp":1762459650235},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662583807"},{"type":"electronic","value":"9783662583814"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-662-58381-4_9","type":"book-chapter","created":{"date-parts":[[2018,11,20]],"date-time":"2018-11-20T09:48:09Z","timestamp":1542707289000},"page":"181-209","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["MCC\u20192017 \u2013 The Seventh Model Checking Contest"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Kordon","sequence":"first","affiliation":[]},{"given":"Hubert","family":"Garavel","sequence":"additional","affiliation":[]},{"given":"Lom Messan","family":"Hillah","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Paviot-Adet","sequence":"additional","affiliation":[]},{"given":"Lo\u00efg","family":"Jezequel","sequence":"additional","affiliation":[]},{"given":"Francis","family":"Hulin-Hubard","sequence":"additional","affiliation":[]},{"given":"Elvio","family":"Amparore","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Beccuti","sequence":"additional","affiliation":[]},{"given":"Bernard","family":"Berthomieu","sequence":"additional","affiliation":[]},{"given":"Hugues","family":"Evrard","sequence":"additional","affiliation":[]},{"given":"Peter G.","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Didier","family":"Le Botlan","sequence":"additional","affiliation":[]},{"given":"Torsten","family":"Liebke","sequence":"additional","affiliation":[]},{"given":"Jeroen","family":"Meijer","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Karsten","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,21]]},"reference":[{"key":"9_CR1","unstructured":"Aldinucci, M., Bagnasco, S., Lusso, S., Pasteris, P., Vallero, S., Rabellino, S.: The open computing cluster for advanced data manipulation (OCCAM). In: 22nd International Conference on Computing in High Energy and Nuclear Physics, San Francisco (2016)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variable-ordering heuristic. In: ACM Great Lakes Symposium on VLSI, pp. 116\u2013119. ACM (2003)","DOI":"10.1145\/764808.764839"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-10696-0_13","volume-title":"Quantitative Evaluation of Systems","author":"EG Amparore","year":"2014","unstructured":"Amparore, E.G.: A new GreatSPN GUI for GSPN editing and CSLTA model checking. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 170\u2013173. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_13"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-68167-2_13","volume-title":"Automated Technology for Verification and Analysis","author":"EG Amparore","year":"2017","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: Gradient-based variable ordering of decision diagrams for systems with structural units. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 184\u2013200. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_13"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Donatelli, S., Beccuti, M., Garbi, G., Miner, A.: Decision diagrams for Petri nets: which variable ordering? In: Petri Net Performance Engineering conference (PNSE), pp. 31\u201350. CEUR-WS (2017)","DOI":"10.1007\/978-3-662-58381-4_4"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-47919-2_13","volume-title":"Petri Nets: Central Models and Their Properties","author":"G Berthelot","year":"1987","unstructured":"Berthelot, G.: Transformations and decompositions of nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 254, pp. 359\u2013376. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/978-3-540-47919-2_13"},{"issue":"14","key":"9_CR7","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and Time Petri nets. Int. J. Prod. Res. 42(14), 2741\u20132756 (2004)","journal-title":"Int. J. Prod. Res."},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-49052-6_2","volume-title":"Hardware and Software: Verification and Testing","author":"V Bloemen","year":"2016","unstructured":"Bloemen, V., van de Pol, J.: Multi-core SCC-based LTL model checking. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 18\u201333. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_2"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/11562436_32","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"J-M Couvreur","year":"2005","unstructured":"Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443\u2013457. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_32"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-28756-5_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2012","unstructured":"David, A., Jacobsen, L., Jacobsen, M., J\u00f8rgensen, K.Y., M\u00f8ller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc Petri nets. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492\u2013497. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_36"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk van","year":"2015","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60"},{"key":"9_CR12","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":"9_CR13","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":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/978-3-662-49674-9_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Evrard","year":"2016","unstructured":"Evrard, H.: DLC: compiling a concurrent system formal specification to a distributed implementation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 553\u2013559. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_34"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-38592-6_11","volume-title":"Formal Techniques for Distributed Systems","author":"H Evrard","year":"2013","unstructured":"Evrard, H., Lang, F.: Formal verification of distributed branching multiway synchronization protocols. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE -2013. LNCS, vol. 7892, pp. 146\u2013160. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38592-6_11"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.jlamp.2016.09.002","volume":"88","author":"H Evrard","year":"2017","unstructured":"Evrard, H., Lang, F.: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous. J. Log. Algebraic Methods Program. 88, 121\u2013153 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"9_CR17","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"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011 a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. (STTT) 15(2), 89\u2013107 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","volume-title":"ModelEd, TestEd, TrustEd","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3\u201326. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68270-9_1"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"230","DOI":"10.4204\/EPTCS.244.10","volume":"244","author":"Hubert Garavel","year":"2017","unstructured":"Garavel, H., Serwe, W.: The unheralded value of the multiway rendezvous: illustration with the production cell benchmark. In: Hermanns, H., H\u00f6fner, P. (eds.) 2nd Workshop on Models for Formal Analysis of Real Systems (MARS). Electronic Proceedings in Theoretical Computer Science, vol. 244, pp. 230\u2013270, April 2017","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"1","key":"9_CR21","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J Geldenhuys","year":"2005","unstructured":"Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-662-53401-4_15","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"A Hamez","year":"2016","unstructured":"Hamez, A.: A symbolic model checker for Petri nets: pnmc. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 297\u2013306. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_15"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-02424-5_20","volume-title":"Applications and Theory of Petri Nets","author":"M Heiner","year":"2009","unstructured":"Heiner, M., Schwarick, M., Tovchigrechko, A.: DSSZ-MC \u2013 a tool for symbolic analysis of extended Petri nets. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 323\u2013332. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02424-5_20"},{"key":"9_CR24","first-page":"9","volume":"76","author":"LM Hillah","year":"2009","unstructured":"Hillah, L.M., Kindler, E., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: A primer on the Petri net markup language and ISO\/IEC 15909\u20132. Petri Net Newslett. 76, 9\u201328 (2009)","journal-title":"Petri Net Newslett."},{"issue":"8","key":"9_CR25","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"9_CR26","unstructured":"ISO\/IEC: High-level Petri Nets - Part 2: Transfer Format. International Standard 15909-2:2011, International Organization for Standardization - Information Technology - Systems and Software Engineering, Geneva (2011)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-53401-4_16","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"JF Jensen","year":"2016","unstructured":"Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P\/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307\u2013318. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_16"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-67729-3_15","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2017","author":"P Jensen","year":"2017","unstructured":"Jensen, P., Larsen, K., Srba, J.: PTrie: data structure for compressing and storing sets via prefix sharing. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 248\u2013265. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67729-3_15"},{"key":"9_CR29","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":"9_CR30","doi-asserted-by":"crossref","unstructured":"Kordon, F., Hulin-Hubard, F.: BenchKit, a tool for massive concurrent benchmarking. In: 14th International Conference on Application of Concurrency to System Design (ACSD 2014), Tunis, Tunisia, pp. 159\u2013165. IEEE Computer Society, June 2014","DOI":"10.1109\/ACSD.2014.12"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35179-2_8","volume-title":"Transactions on Petri Nets and Other Models of Concurrency VI","author":"F Kordon","year":"2012","unstructured":"Kordon, F., et al.: Report on the model checking contest at Petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169\u2013196. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35179-2_8"},{"key":"9_CR32","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"},{"issue":"2","key":"9_CR33","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (1998)","journal-title":"ACM Trans. Comput. Syst."},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-13338-6_16","volume-title":"Hardware and Software: Verification and Testing","author":"J Meijer","year":"2014","unstructured":"Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 204\u2013219. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_16"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-40648-0_20","volume-title":"NASA Formal Methods","author":"J Meijer","year":"2016","unstructured":"Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 255\u2013271. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-13675-7_16","volume-title":"Applications and Theory of Petri Nets","author":"O Oanea","year":"2010","unstructured":"Oanea, O., Wimmel, H., Wolf, K.: New algorithms for deciding the Siphon-Trap property. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 267\u2013286. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13675-7_16"},{"key":"9_CR37","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: USENIX Annual Technical Conference (USENIX ATC), pp. 305\u2013319. USENIX Association (2014)"},{"issue":"7","key":"9_CR38","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s002360050002","volume":"36","author":"K Schmidt","year":"2000","unstructured":"Schmidt, K.: How to calculate symmetries of Petri nets. Acta Informaticae 36(7), 545\u2013590 (2000)","journal-title":"Acta Informaticae"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Sorensen, T., Evrard, H., Donaldson, A.F.: Cooperative kernels: GPU multitasking for blocking algorithms. In: Bodden, E., Sch\u00e4fer, W., van Deursen, A., Zisman, A. (eds.) 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE, pp. 431\u2013441. ACM (2017)","DOI":"10.1145\/3106237.3106265"},{"key":"9_CR40","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"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci. 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:27)2012"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XIII"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-58381-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T14:42:24Z","timestamp":1572964944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-58381-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783662583807","9783662583814"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-58381-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}