{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T00:04:52Z","timestamp":1774915492447,"version":"3.50.1"},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s10009-021-00615-1","type":"journal-article","created":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T06:09:11Z","timestamp":1622527751000},"page":"931-952","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019"],"prefix":"10.1007","volume":"23","author":[{"given":"Fabrice","family":"Kordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lom Messan","family":"Hillah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francis","family":"Hulin-Hubard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lo\u00efg","family":"Jezequel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Paviot-Adet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,1]]},"reference":[{"key":"615_CR1","unstructured":"Amendola, G., Ricca, F., Truszczynski, M.: A generator of hard 2qbf formulas and ASP programs. In: 16th International Conference on Principles of Knowledge Representation and Reasoning, pp. 52\u201356. AAAI Press (2018)"},{"key":"615_CR2","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Principles of Performance and Reliability Modeling and Evaluation, pp. 227\u2013254. Springer (2016)","DOI":"10.1007\/978-3-319-30599-8_9"},{"key":"615_CR3","doi-asserted-by":"crossref","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, Lecture Notes in Computer Science, vol. 9450, pp. 79\u201387. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_6"},{"key":"615_CR4","doi-asserted-by":"crossref","unstructured":"Babar, J., Beccuti, M., Donatelli, S., Miner, A.S.: GreatSPN Enhanced with Decision Diagram Data Structures. In: 31st International Conference on Applications and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 6128, pp. 308\u2013317. Springer (2010)","DOI":"10.1007\/978-3-642-13675-7_19"},{"key":"615_CR5","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: Sat challenge 2012 (2012). https:\/\/baldur.iti.kit.edu\/SAT-Challenge-2012"},{"key":"615_CR6","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.artint.2015.01.002","volume":"223","author":"A Balint","year":"2015","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: Overview and analysis of the SAT challenge 2012 solver competition. Artificual Intelligence 223, 120\u2013155 (2015)","journal-title":"Artificual Intelligence"},{"key":"615_CR7","doi-asserted-by":"crossref","unstructured":"Barrett, C., de\u00a0Moura, L., Stump, A.: Smt-comp: Satisfiability modulo theories competition. In: 17th International Conference on Computer Aided Verification\u2014CAV, Lecture Notes in Computer Science, vol. 3576, pp. 20\u201323. Springer (2005)","DOI":"10.1007\/11513988_4"},{"key":"615_CR8","doi-asserted-by":"crossref","unstructured":"Berthelot, G., Roucairol, G.: Reduction of Petri Nets. In: 5th Symposium on Mathematical Foundations of Computer Science 1976, Lecture Notes in Computer Science, vol.\u00a045, pp. 202\u2013209. Springer (1976)","DOI":"10.1007\/3-540-07854-1_175"},{"key":"615_CR9","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Botlan, D.L., Dal-Zilio, S.: Petri net reductions for counting markings. In: 25th International Symposium on Model Checking Software (SPIN), Lecture Notes in Computer Science, vol. 10869, pp. 65\u201384. Springer (2018)","DOI":"10.1007\/978-3-319-94111-0_4"},{"issue":"14","key":"615_CR10","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. In. J. Prod. Res. 42(14), 2741\u20132756 (2004)","journal-title":"In. J. Prod. Res."},{"key":"615_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.): Tools and Algorithms for the Construction and Analysis of Systems\u201425 Years of TACAS: TOOLympics. Lecture Notes in Computer Science, vol. 11429. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3"},{"issue":"1","key":"615_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"615_CR13","doi-asserted-by":"crossref","unstructured":"Beyer, D., Wendler, P.: CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 12079, pp. 126\u2013133. Springer (2020)","DOI":"10.1007\/978-3-030-45237-7_8"},{"key":"615_CR14","doi-asserted-by":"crossref","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: FMCAD, p.\u00a09. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"615_CR15","unstructured":"Bj\u00f8rner, N., Benney, E., Gupta, A., Horrocks, I., Iannni, G., Le Berre, D., Wakdmann, J.: Starexec (2020). https:\/\/www.starexec.org\/starexec\/public\/about.jsp"},{"key":"615_CR16","doi-asserted-by":"crossref","unstructured":"B\u00f8nneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of petri nets. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency, Lecture Notes in Computer Science, vol. 10877, pp. 143\u2013163. Springer (2018)","DOI":"10.1007\/978-3-319-91268-4_8"},{"issue":"8","key":"615_CR17","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"615_CR18","doi-asserted-by":"crossref","unstructured":"Buchs, D., Klikovits, S., Linard, A., Mencattini, R., Racordon, D.: A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency, Lecture Notes in Computer Science, vol. 10877, pp. 385\u2013395. Springer (2018)","DOI":"10.1007\/978-3-319-91268-4_21"},{"key":"615_CR19","doi-asserted-by":"crossref","unstructured":"Burch, J., Clarke, E., McMillan, K.: Symbolic model checking: $$10^{20}$$ states and beyond. Information and Computation (Special issue for best papers from LICS90) 98(2), 153\u2013181 (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"issue":"1\u20132","key":"615_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0304-3975(96)00010-2","volume":"176","author":"G Chiola","year":"1997","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured Petri nets. Theor. Comput. Sci. 176(1\u20132), 39\u201365 (1997)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"615_CR21","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1530873.1530885","volume":"36","author":"G Ciardo","year":"2009","unstructured":"Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS Perform. Eval. Rev. 36(4), 58\u201363 (2009)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"1","key":"615_CR22","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Sys. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Sys. Des."},{"key":"615_CR23","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: 12th International Conference on Computer Aided Verification\u2014CAV, Lecture Notes in Computer Science, vol. 1855, pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"key":"615_CR24","doi-asserted-by":"crossref","unstructured":"Colange, M., Hillah, L.M., Kordon, F., Parutto, P.: Extreme Symmetries in Complex Distributed Systems: the Bag-Oriented Approach. In: 17th Monterey Workshop : Development. Operation and Management of Large-Scale Complex IT Systems, Revised Selected Papers, Lecture Notes in Computer Science, vol. 7539, pp. 330\u2013352. Springer, Oxford, UK (2012)","DOI":"10.1007\/978-3-642-34059-8_17"},{"key":"615_CR25","doi-asserted-by":"crossref","unstructured":"Couvreur, J., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: 25th International Conference on Formal Techniques for Networked and Distributed Systems\u2014FORTE, Lecture Notes in Computer Science, vol. 3731, pp. 443\u2013457. Springer (2005)","DOI":"10.1007\/11562436_32"},{"key":"615_CR26","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: 14th International Symposium on Automated Technology for Verification and Analysis\u2014ATVA, Lecture Notes in Computer Science, vol. 9938, pp. 122\u2013129 (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"615_CR27","unstructured":"enPAC git-hug page (2020). https:\/\/github.com\/Tj-Cong\/enPAC"},{"key":"615_CR28","doi-asserted-by":"crossref","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: Verifythis\u2014verification competition with a human factor. In: Tools and Algorithms for the Construction and Analysis of Systems\u201425 Years of TACAS: TOOLympics, Lecture Notes in Computer Science, vol. 11429, pp. 176\u2013195. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_12"},{"key":"615_CR29","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hoffmann, P.: Reduction rules for colored workflow nets. In: 19th International Conference on Fundamental Approaches to Software Engineering\u2014FASE (ETAPS), Lecture Notes in Computer Science, vol. 9633, pp. 342\u2013358. Springer (2016)","DOI":"10.1007\/978-3-662-49665-7_20"},{"key":"615_CR30","doi-asserted-by":"crossref","unstructured":"Esparza, J., Schr\u00f6ter, C.: Net reductions for LTL model-checking. In: 11th IFIP WG 10.5 conference in Correct Hardware Design and Verification Methods CHARME, Lecture Notes in Computer Science, vol. 2144, pp. 310\u2013324. Springer (2001)","DOI":"10.1007\/3-540-44798-9_25"},{"key":"615_CR31","doi-asserted-by":"crossref","unstructured":"Fehling, R.: A concept of hierarchical petri nets with building blocks. In: Advances in Petri Nets, Lecture Notes in Computer Science, vol. 674, pp. 148\u2013168. Springer (1993)","DOI":"10.1007\/3-540-56689-9_43"},{"key":"615_CR32","doi-asserted-by":"crossref","unstructured":"Garavel, H.: Nested-Unit Petri Nets: A structural means to increase efficiency and scalability of verification on elementary nets. In: International Conference on Application and Theory of Petri Nets and Concurrency, LNCS, vol. 9115, pp. 179\u2013199. Springer (2015)","DOI":"10.1007\/978-3-319-19488-2_9"},{"key":"615_CR33","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlamp.2018.11.005","volume":"104","author":"H Garavel","year":"2019","unstructured":"Garavel, H.: Nested-unit petri nets. J. Log. Algebr. Meth. Program. 104, 60\u201385 (2019)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"615_CR34","unstructured":"Girault, C., Valk, R.: Petri nets for systems engineering - a guide to modeling, verification, and applications. Springer (2003). http:\/\/www.springer.com\/computer\/swe\/book\/978-3-540-41217-5"},{"key":"615_CR35","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Peled, D.A., Staskauskas, M.G.: Using partial-order methods in the formal validation of industrial concurrent programs. In: International Symposium on Software Testing and Analysis \u2013 ISSTA, pp. 261\u2013269. ACM (1996)","DOI":"10.1145\/226295.226324"},{"key":"615_CR36","doi-asserted-by":"crossref","unstructured":"Haddad, S.: A reduction theory for coloured nets. In: Advances in Petri Nets 1989, covers the 9th European Workshop on Applications and Theory in Petri Nets, held in Venice, Italy in June 1988, selected papers, Lecture Notes in Computer Science, vol. 424, pp. 209\u2013235. Springer (1990)","DOI":"10.1007\/3-540-52494-0_31"},{"key":"615_CR37","doi-asserted-by":"crossref","unstructured":"Haddad, S.: Introduction: issues in verification. In: C.\u00a0Girault, R.\u00a0Valk (eds.) Petri Nets for Systems Engineering, A Guide to Modeling, Verification, and Applications, pp. 183\u2013200 (2003)","DOI":"10.1007\/978-3-662-05324-9_14"},{"key":"615_CR38","doi-asserted-by":"crossref","unstructured":"Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J.F., Tr\u00e8ves, N.: Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains. In: 28th American Control Conference\u2014ACC, pp. 5018\u20135025. Omnipress IEEE, St-Louis, USA (2009)","DOI":"10.1109\/ACC.2009.5160020"},{"key":"615_CR39","doi-asserted-by":"crossref","unstructured":"Hamez, A.: A Symbolic Model Checker for Petri Nets: pnmc. Transactions on Petri Nets and Other Models of Concurrency XI 297\u2013306, (2016)","DOI":"10.1007\/978-3-662-53401-4_15"},{"key":"615_CR40","doi-asserted-by":"crossref","unstructured":"Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: Marcie\u2019s secrets of efficient model checking. Transactions on Petri Nets and Other Models of Concurrency XI 286\u2013296, (2016)","DOI":"10.1007\/978-3-662-53401-4_14"},{"key":"615_CR41","doi-asserted-by":"crossref","unstructured":"Hillah, L., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PN standardisation : a survey. In: International Conference on Formal Methods for Networked and Distributed Systems\u2014FORTE. Lecture Notes in Computer Science, vol. 4229, pp. 307\u2013322. Springer Verlag, Paris, France (2006)","DOI":"10.1007\/11888116_23"},{"key":"615_CR42","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 Newsl. 76, 9\u201328 (2009)","journal-title":"Petri Net Newsl."},{"key":"615_CR43","doi-asserted-by":"crossref","unstructured":"Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a hierarchical static order for decision diagram-based representation from P\/T nets. Transactions on Petri Nets and Other Models of Concurrency V 121\u2013140, (2012)","DOI":"10.1007\/978-3-642-29072-5_5"},{"key":"615_CR44","doi-asserted-by":"crossref","unstructured":"Jasper, M., Mues, M., Murtovi, A., Schl\u00fcter, M., Howar, F., Steffen, B., Schordan, M., Hendriks, D., Schiffelers, R.R.H., Kuppens, H., Vaandrager, F.W.: RERS 2019: Combining synthesis with real-world models. In: Tools and Algorithms for the Construction and Analysis of Systems\u201425 Years of TACAS: TOOLympics, Lecture Notes in Computer Science, vol. 11429, pp. 101\u2013115. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_7"},{"key":"615_CR45","doi-asserted-by":"crossref","unstructured":"Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P\/T nets. Transactions on Petri Nets and Other Models of Concurrency XI 307\u2013318, (2016)","DOI":"10.1007\/978-3-662-53401-4_16"},{"key":"615_CR46","doi-asserted-by":"crossref","unstructured":"Jensen, P.G., Larsen, K.G., Srba, J.: PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing. In: 14th International Colloquium on Theoretical Aspects of Computing\u2014ICTAC, Lecture Notes in Computer Science, vol. 10580, pp. 248\u2013265. Springer (2017)","DOI":"10.1007\/978-3-319-67729-3_15"},{"key":"615_CR47","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: Ltsmin: High-performance language-independent model checking. In: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u2014TACAS (ETAPS), Lecture Notes in Computer Science, vol. 9035, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"615_CR48","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L., Paviot-Adet, E., Jezequel, L., Hulin-Hubard, F., Amparore, E.G., Beccuti, M., Berthomieu, B., Evrard, H., Jensen, P.G., Botlan, D.L., Liebke, T., Meijer, J., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: Mcc\u20192017\u2014the seventh model checking contest. Transactions on Petri Nets and Other Models of Concurrency XIII 181\u2013209, (2018)","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"615_CR49","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., J\u00e9z\u00e9quel, L., Paviot-adet, E.: The Model Checking Contest (2019). https:\/\/mcc.lip6.fr"},{"key":"615_CR50","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\u2014ACSD, pp. 159\u2013165. IEEE Computer Society (2014)","DOI":"10.1109\/ACSD.2014.12"},{"key":"615_CR51","doi-asserted-by":"crossref","unstructured":"Kordon, F., Leuschel, M., van\u00a0de Pol, J., Thierry-Mieg, Y.: Software Architecture of Modern Model Checkers. In: B.\u00a0Steffen, G.J. Woeginger (eds.) Computing and Software Science\u2014State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 393\u2013419. Springer (2019)","DOI":"10.1007\/978-3-319-91908-9_20"},{"key":"615_CR52","unstructured":"Kordon, F., Peyre, J.F.: Process decomposition for Rapid Prototyping of Parallel systems. In: Proceedings of the 6th International Symposium on Computer and Information Science, Kener, Antalya, Turkey (1991)"},{"key":"615_CR53","unstructured":"Kordon, F., van de Pol, J., Seidl, M.: Lorentz workshop, advancing verification competitions as a scientific method (2019)"},{"key":"615_CR54","doi-asserted-by":"crossref","unstructured":"Le, D., Nguyen, H., Nguyen, V., Mai, P., Pham-Duy, B., Quan, T., Andr\u00e9, \u00c9., Petrucci, L., Liu, Y.: Pecan: Compositional verification of petri nets made easy. In: 12th International Symposium on Automated Technology for Verification and Analysis\u2014ATVA, Lecture Notes in Computer Science, vol. 8837, pp. 242\u2013247. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_18"},{"key":"615_CR55","doi-asserted-by":"crossref","unstructured":"Leino, R.: Dafny: An automatic program verifier for functional correctness. In: 16th International Conference on Logic Programming and Automated Reasoning\u2014LPAR, Lecture Notes in Artificial Intelligence, vol. 6355, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"615_CR56","doi-asserted-by":"crossref","unstructured":"L\u00f3pez B\u00f3beda, E., Colange, M., Buchs, D.: Stratagem: A generic petri net verification framework. In: 35th International Conference on Application and Theory of Petri Nets and Concurrency\u2014PETRI NETS. Lecture Notes in Computer Science, vol. 8489, pp. 364\u2013373. Springer, Tunis, Tunisia (2014)","DOI":"10.1007\/978-3-319-07734-5_20"},{"key":"615_CR57","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: 9th Annual ACM Symposium on Principles of Distributed Computing\u2014PODC, pp. 377\u2013410. ACM (1990)","DOI":"10.1145\/93385.93442"},{"issue":"1","key":"615_CR58","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"KL McMillan","year":"1995","unstructured":"McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 45\u201365 (1995)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"615_CR59","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"615_CR60","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: Ranking and reputation systems in the qbf competition. In: AI*IA 2007: Artificial Intelligence and Human-Oriented Computing, Lecture Notes in Artificial Intelligence, vol. 4733, pp. 97\u2013108. Springer (2007)","DOI":"10.1007\/978-3-540-74782-6_10"},{"key":"615_CR61","doi-asserted-by":"crossref","unstructured":"Peled, D.A.: All from one, one for all: on model checking using representatives. In: 5th International Conference on Computer Aided Verification\u2014CAV, Lecture Notes in Computer Science, vol. 697, pp. 409\u2013423. Springer (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"615_CR62","doi-asserted-by":"crossref","unstructured":"Racordon, D., Buchs, D.: Verifying multi-core schedulability with data decision diagrams. In: 8th International Workshop on Software Engineering for Resilient Systems\u2014SERENE, Lecture Notes in Computer Science, vol. 9823, pp. 45\u201361. Springer (2016)","DOI":"10.1007\/978-3-319-45892-2_4"},{"key":"615_CR63","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, C., Schwoon, S.: Cunf: A tool for unfolding and verifying Petri Nets with Read Arcss. In: 11th International Symposium on Automated Technology for Verification and Analysis\u2014ATVA, Lecture Notes in Computer Science, vol. 8172, pp. 492\u2013495. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_42"},{"key":"615_CR64","doi-asserted-by":"crossref","unstructured":"Runeson, P., H\u00f6st, M.: Guidelines for conducting and reporting case study research in software engineering. Empir. Softw. Eng. 14(2), 131\u2013164 (2009)","DOI":"10.1007\/s10664-008-9102-8"},{"issue":"1\u20132","key":"615_CR65","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B Selman","year":"1996","unstructured":"Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artif. Intell. 81(1\u20132), 17\u201329 (1996)","journal-title":"Artif. Intell."},{"key":"615_CR66","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M., Meijer, J., van\u00a0de Pol, J.: Property-preserving generation of tailored benchmark petri nets. In: 17th International Conference on Application of Concurrency to System Design\u2014CSD, pp. 1\u20138. IEEE Computer Society (2017)","DOI":"10.1109\/ACSD.2017.24"},{"key":"615_CR67","doi-asserted-by":"publisher","first-page":"419","DOI":"10.3233\/AIC-170744","volume":"30","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The cade-26 automated theorem proving system competition\u2014CASC-26. AI Commun. 30, 419\u2013432 (2017)","journal-title":"AI Commun."},{"key":"615_CR68","doi-asserted-by":"crossref","unstructured":"Thierry-Mieg, Y.: Symbolic Model-Checking Using ITS-Tools. In: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u2014TACAS (ETAPS), Lecture Notes in Computer Science, vol. 9035, pp. 231\u2013237. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"615_CR69","doi-asserted-by":"crossref","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u2014TACAS (ETAPS), Lecture Notes in Computer Science, vol. 5505, pp. 1\u201315. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_1"},{"key":"615_CR70","unstructured":"The international SAT competition web page (2020). http:\/\/www.satcompetition.org"},{"key":"615_CR71","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.: Multi-core decision diagrams. In: Y.\u00a0Hamadi, L.\u00a0Sais (eds.) Handbook of Parallel Constraint Reasoning., pp. 509\u2013545 (2018)","DOI":"10.1007\/978-3-319-63516-3_13"},{"key":"615_CR72","doi-asserted-by":"crossref","unstructured":"Valk, R.: Object petri nets. In: Advances in Petri Nets, Lecture Notes in Computer Science, vol. 3098, pp. 819\u2013848. Springer (2004)","DOI":"10.1007\/978-3-540-27755-2_23"},{"key":"615_CR73","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Computer Aided Verification, 2nd International Workshop\u2014CAV, Lecture Notes in Computer Science, vol. 531, pp. 156\u2013165. Springer (1991)","DOI":"10.1007\/BFb0023729"},{"key":"615_CR74","doi-asserted-by":"crossref","unstructured":"Wolf, K.: Petri Net Model Checking with LoLA 2. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency\u2014PETRI NETS, Lecture Notes in Computer Science, vol. 10877, pp. 351\u2013362. Springer (2018)","DOI":"10.1007\/978-3-319-91268-4_18"},{"key":"615_CR75","doi-asserted-by":"crossref","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: 15th International Conference on Theory and Applications of Satisfiability Testing\u2014SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 228\u2013241. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_18"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00615-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00615-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00615-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:03:37Z","timestamp":1640520217000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00615-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,1]]},"references-count":75,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["615"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00615-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,1]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}