{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:19:25Z","timestamp":1773105565941,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642351785","type":"print"},{"value":"9783642351792","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35179-2_8","type":"book-chapter","created":{"date-parts":[[2012,11,14]],"date-time":"2012-11-14T02:20:42Z","timestamp":1352859642000},"page":"169-196","source":"Crossref","is-referenced-by-count":26,"title":["Report on the Model Checking Contest at Petri Nets 2011"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Kordon","sequence":"first","affiliation":[]},{"given":"Alban","family":"Linard","sequence":"additional","affiliation":[]},{"given":"Didier","family":"Buchs","sequence":"additional","affiliation":[]},{"given":"Maximilien","family":"Colange","sequence":"additional","affiliation":[]},{"given":"Sami","family":"Evangelista","sequence":"additional","affiliation":[]},{"given":"Kai","family":"Lampka","sequence":"additional","affiliation":[]},{"given":"Niels","family":"Lohmann","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Paviot-Adet","sequence":"additional","affiliation":[]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[]},{"given":"Harro","family":"Wimmel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","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\/764825.764839"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/978-3-540-47919-2_13","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"G. Berthelot","year":"1987","unstructured":"Berthelot, G.: Transformations and Decompositions of Nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0254, pp. 359\u2013376. Springer, Heidelberg (1987)"},{"key":"8_CR3","unstructured":"Buchs, D., Hostettler, S.: Sigma Decision Diagrams. In: Preliminary Proceedings of the 5th International Workshop on Computing with Terms and Graphs, pp. 18\u201332. No. TR-09-05 in TERMGRAPH workshops, Universit\u00e0 di Pisa (2009)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-12002-2_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Buchs","year":"2010","unstructured":"Buchs, D., Hostettler, S., Marechal, A., Risoldi, M.: AlPiNA: An Algebraic Petri Net Analyzer. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 349\u2013352. Springer, Heidelberg (2010)"},{"key":"8_CR5","first-page":"49","volume-title":"International Conference on Very Large Scale Integration","author":"J. Burch","year":"1991","unstructured":"Burch, J., Clarke, E., Long, D.: Symbolic Model Checking with Partitioned Transition Relations. In: Halaas, A., Denyer, P.B. (eds.) International Conference on Very Large Scale Integration, pp. 49\u201358. North-Holland, Edinburgh (1991)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: On well-formed coloured nets and their symbolic reachability graph. In: Jensen, K., Rozenberg, G. (eds.) Proceedings of the 11th International Conference on Application and Theory of Petri Nets, ICATPN 1990. Reprinted in High-Level Petri Nets, Theory and Application. Springer (1991)","DOI":"10.1007\/978-3-642-84524-6_13"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Chiola, G., Franceschinis, G.: Colored GSPN Models and Automatic Symmetry Detection. In: The Proceedings of the Third International Workshop on Petri Nets and Performance Models, PNPM 1989, pp. 50\u201360. IEEE Computer Society (1989)","DOI":"10.1109\/PNPM.1989.68539"},{"key":"8_CR8","unstructured":"Ciardo, G.: Advances in compositional approaches based on kronecker algebra: Application to the study of manufacturing systems. In: 3rd International Workshop on Performability Modeling of Computer and Communication Systems, pp. 61\u201365 (1996)"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G. Ciardo","year":"1993","unstructured":"Ciardo, G., Trivedi, K.: A decomposition approach for stochastic reward net models. Perf. Eval.\u00a018, 37\u201359 (1993)","journal-title":"Perf. Eval."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Application and Theory of Petri Nets 2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Efficient Symbolic State-Space Construction for Asynchronous Systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 103\u2013122. Springer, Heidelberg (2000)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-21834-7_20","volume-title":"Applications and Theory of Petri Nets","author":"M. Colange","year":"2011","unstructured":"Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Crocodile: A Symbolic\/Symbolic Tool for the Analysis of Symmetric Nets with Bag. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol.\u00a06709, pp. 338\u2013347. Springer, Heidelberg (2011)"},{"key":"8_CR13","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.\u00a03731, pp. 443\u2013457. Springer, Heidelberg (2005)"},{"issue":"11","key":"8_CR14","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"E.W. Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM\u00a017(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design\u00a016, 159\u2013189 (2000)","journal-title":"Formal Methods in System Design"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/11494744_26","volume-title":"Applications and Theory of Petri Nets 2005","author":"S. Evangelista","year":"2005","unstructured":"Evangelista, S.: High Level Petri Nets Analysis with Helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol.\u00a03536, pp. 455\u2013464. Springer, Heidelberg (2005)"},{"key":"8_CR17","unstructured":"Finnemann, J., Nielsen, T., K\u00e6rlund, L.: Petri nets with discrete variables. Tech. rep. (2011), http:\/\/jopsen.dk\/downloads\/PetriNetsWithDiscreteVariables.pdf"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"5018","DOI":"10.1109\/ACC.2009.5160020","volume-title":"28th American Control Conference, ACC 2009","author":"S. Haddad","year":"2009","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, ACC 2009, pp. 5018\u20135025. Omnipress IEEE, St-Louis (2009)"},{"issue":"3-4","key":"8_CR19","doi-asserted-by":"crossref","first-page":"413","DOI":"10.3233\/FI-2009-137","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. Fundamenta Informaticae\u00a094(3-4), 413\u2013437 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-68894-5_7","volume-title":"Formal Methods for Computational Systems Biology","author":"M. Heiner","year":"2008","unstructured":"Heiner, M., Gilbert, D., Donaldson, R.: Petri Nets for Systems and Synthetic Biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol.\u00a05016, pp. 215\u2013264. Springer, Heidelberg (2008)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-29072-5_5","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"S. Hong","year":"2012","unstructured":"Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a Hierarchical Static Order for Decision Diagram-Based Representation from P\/T Nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol.\u00a06900, pp. 121\u2013140. Springer, Heidelberg (2012)"},{"key":"8_CR22","unstructured":"Hostettler, S., Linard, A., Marechal, A., Risoldi, M.: Improving the significance of benchmarks for petri nets model checkers. In: 1st International Workshop on Scalable and Usable Model Checking for Petri Nets and Other Models of Concurrency, pp. 97\u2013111 (2010)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Hostettler, S., Marechal, A., Linard, A., Risoldi, M., Buchs, D.: High-Level Petri Net Model Checking with AlPiNA. Fundamenta Informaticae 113 (2011)","DOI":"10.3233\/FI-2011-608"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st Verified Software Competition: Experience Report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/11888116_25","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"F. Kordon","year":"2006","unstructured":"Kordon, F., Linard, A., Paviot-Adet, E.: Optimized Colored Nets Unfolding. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol.\u00a04229, pp. 339\u2013355. Springer, Heidelberg (2006)"},{"issue":"3","key":"8_CR26","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10703-006-0006-1","volume":"29","author":"L.M. Kristensen","year":"2006","unstructured":"Kristensen, L.M., Schmidt, K., Valmari, A.: Question-guided Stubborn Set Methods for State Properties. Formal Methods in System Design\u00a029(3), 215\u2013251 (2006)","journal-title":"Formal Methods in System Design"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/3-540-44988-4_17","volume-title":"Application and Theory of Petri Nets 2000","author":"L.M. Kristensen","year":"2000","unstructured":"Kristensen, L.M., Valmari, A.: Improved Question-Guided Stubborn Set Methods for State Properties. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 282\u2013302. Springer, Heidelberg (2000)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Lampka, K.: A new algorithm for partitioned symbolic reachability analysis. In: Workshop on Reachability Problems. ENTCS, vol.\u00a0223 (2008)","DOI":"10.1016\/j.entcs.2008.12.036"},{"key":"8_CR29","unstructured":"Lampka, K., Siegle, M.: Activity-Local State Graph Generation for High-Level Stochastic Models. In: Measuring, Modelling, and Evaluation of Systems 2006, pp. 245\u2013264 (2006)"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/j.entcs.2008.12.036","volume":"223","author":"K. Lampka","year":"2008","unstructured":"Lampka, K.: A new algorithm for partitioned symbolic reachability analysis. Electron. Notes Theor. Comput. Sci.\u00a0223, 137\u2013151 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR31","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/s10703-010-0095-8","volume":"36","author":"K. Lampka","year":"2010","unstructured":"Lampka, K., Siegle, M., Ossowski, J., Baier, C.: Partially-shared zero-suppressed multi-terminal bdds: concept, algorithms and applications. Formal Methods in System Design\u00a036, 198\u2013222 (2010)","journal-title":"Formal Methods in System Design"},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1109\/ACSD.2010.17","volume-title":"10th International Conference on Application of Concurrency to System Design, ACSD 2010","author":"A. Linard","year":"2010","unstructured":"Linard, A., Paviot-Adet, E., Kordon, F., Buchs, D., Charron, S.: polyDD: Towards a Framework Generalizing Decision Diagrams. In: 10th International Conference on Application of Concurrency to System Design, ACSD 2010, pp. 124\u2013133. IEEE Computer Society, Braga (2010)"},{"key":"8_CR33","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1145\/157485.164890","volume-title":"Proc. of the 30th Design Automation Conference, DAC","author":"S. Minato","year":"1993","unstructured":"Minato, S.: Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems. In: Proc. of the 30th Design Automation Conference, DAC, pp. 272\u2013277. ACM\/IEEE, Dallas (Texas), USA (1993)"},{"key":"8_CR34","unstructured":"Pastor, E., Roig, O., Cortadella, J.: Symbolic Petri Net Analysis using Boolean Manipulation, Technical Report of Departament Arquitectura de Computadors (UPC) DAC\/UPC Report No. 97\/8 (1997)"},{"issue":"3","key":"8_CR35","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett.\u00a012(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"issue":"3-4","key":"8_CR36","first-page":"325","volume":"47","author":"K. Schmidt","year":"2001","unstructured":"Schmidt, K.: Narrowing petri net state spaces using the state equation. Fundamenta Informaticae\u00a047(3-4), 325\u2013335 (2001)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-48745-X_4","volume-title":"Application and Theory of Petri Nets 1999","author":"K. Schmidt","year":"1999","unstructured":"Schmidt, K.: Stubborn Sets for Standard Properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 46\u201365. Springer, Heidelberg (1999)"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/3-540-36577-X_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Schmidt","year":"2003","unstructured":"Schmidt, K.: Using Petri Net Invariants in State Space Construction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 473\u2013488. Springer, Heidelberg (2003)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-30232-2_18","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"Y. Thierry-Mieg","year":"2004","unstructured":"Thierry-Mieg, Y., Ili\u00e9, J.-M., Poitrenaud, D.: A Symbolic Symbolic State Space Representation. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 276\u2013291. Springer, Heidelberg (2004)"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00768-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Thierry-Mieg","year":"2009","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical Set Decision Diagrams and Regular Models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 1\u201315. Springer, Heidelberg (2009)"},{"key":"8_CR41","unstructured":"Wikipedia: Dining philosophers problem (2011), http:\/\/en.wikipedia.org\/wiki\/Dining_philosophers_problem"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-19835-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Wimmel","year":"2011","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri Net State Equation. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 224\u2013238. Springer, Heidelberg (2011)"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-540-73094-1_5","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"K. Wolf","year":"2007","unstructured":"Wolf, K.: Generating Petri Net State Spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 29\u201342. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35179-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T21:03:28Z","timestamp":1745183008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35179-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351785","9783642351792"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35179-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}