{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T07:44:22Z","timestamp":1789199062075,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540423454","type":"print"},{"value":"9783540445852","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_28","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T19:39:50Z","timestamp":1265917190000},"page":"298-310","source":"Crossref","is-referenced-by-count":22,"title":["Attacking Symbolic State Explosion"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Van Begin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"28_CR1","unstructured":"ABC+95._M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. Series in Parallel Computing. John Wiley & Sons, 1995."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla and A. Nyl\u00e9n. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proc. LICS 2000, pages 132\u2013140, 2000.","DOI":"10.1109\/LICS.2000.855762"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS\u2019 96, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"28_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"MSR Technical Report 2000-116","author":"T. Ball","year":"2001","unstructured":"T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. MSR Technical Report 2000-116. In Proc. TACAS 2001, LNCS 2031, pages 158\u2013173, 2001."},{"key":"28_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Efficient Timed Reachability Analysis Using Clock Difference Diagrams","author":"B.L.P.+.9.9._.G. Behrmann","year":"1999","unstructured":"BLP+99._G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proc. CAV\u2019 99, LNCS 1633, pages 341\u2013353, 1999."},{"key":"28_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"Reachability analysis of (timed) Petri nets using real arithmeti","author":"B. B\u00e9rard","year":"1999","unstructured":"B. B\u00e9rard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmeti In Proc. CONCUR\u2019 99, LNCS 1664, pages 178\u2013193, 1999."},{"key":"28_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"Model Checking Lossy Vector Addition Systems","author":"A. Bouajjani","year":"1999","unstructured":"A. Bouajjani, and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proc. STACS\u2019 99, LNCS 1563, pages 323\u2013333, 1999."},{"key":"28_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/3-540-46419-0_30","volume-title":"BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems","author":"T. Bultan","year":"2000","unstructured":"T. Bultan. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. In Proc. TACAS 2000, LNCS 1785, pages 441\u2013455, 2000."},{"key":"28_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics. In Proc. CAV\u2019 97, LNCS 1254, pages 400\u2013411, 1997."},{"issue":"1\u20132","key":"28_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0166-5316(95)00008-L","volume":"24","author":"G. Chiola","year":"1995","unstructured":"G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo. GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets. Performance Evaluation, 24(1\u20132), pages 47\u201368, 1995.","journal-title":"Performance Evaluation"},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","first-page":"53","volume-title":"Automatic Verification of Parameterized Cache Coherence Protocols","author":"G. Delzanno","year":"1996","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV 2000, LNCS 1855, pages 53\u201368, 1996."},{"key":"28_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Constraint-based Analysis of Broadcast Protocols","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. CSL\u2019 99, LNCS 1683, pag. 50\u201366, 1999."},{"key":"28_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-46419-0_29","volume-title":"Symbolic Representation of Upward-closed Sets","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno, and J. F. Raskin. Symbolic Representation of Upward-closed Sets. In Proc. TACAS 2000, LNCS 1785, pages 426\u2013440, 2000."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proc. LICS\u2019 98, pages 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS\u2019 99, pages 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"28_CR16","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J. Esparza","year":"2000","unstructured":"J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159\u2013189, 2000.","journal-title":"Formal Methods in System Design"},{"key":"28_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-56689-9_45","volume-title":"In Advances in Petri Nets\u2019 93","author":"A. Finkel","year":"1993","unstructured":"A. Finkel. The minimal coverability graph for Petri nets. In In Advances in Petri Nets\u2019 93, LNCS 674, pages 210\u2013243. Springer, 1993."},{"issue":"1\u20132","key":"28_CR18","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1\u20132):63\u201392, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"28_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675\u2013735 (1992)","journal-title":"JACM"},{"key":"28_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"HyTech: a Model Checker for Hybrid Systems","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a Model Checker for Hybrid Systems. In Proc. CAV\u2019 97, LNCS 1254, pages 460\u2013463, 1997."},{"key":"28_CR21","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Symbolic Model Checking with Rich Assertional Languages","author":"K.M.M.+.9.7._.Y. Kesten","year":"1997","unstructured":"KMM+97._Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV\u2019 97, LNCS 1254, pages 424\u2013435, 1997."},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"A. Miner, and G. Ciardo. Efficient Reachability Set Generation and Storage using Decision Diagrams. In Proc. of ICATPN\u2019 99, pages 6\u201325, 1999.","DOI":"10.1007\/3-540-48745-X_2"},{"key":"28_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/3-540-48745-X_3","volume-title":"Structural Methods to Improve the Symbolic Analysis of Petri Nets","author":"E. Pastor","year":"1999","unstructured":"E. Pastor, J. Cortadella, M. A. Pe\u00f1a. Structural Methods to Improve the Symbolic Analysis of Petri Nets. In Proc. ICATPN\u2019 99, LNCS 1639, pages 26\u201345. Springer, 1999."},{"key":"28_CR24","unstructured":"W. Reisig. Petri Nets. An introduction. EATCS Monographs on Theoretical Computer Science, Springer 1986."},{"key":"28_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/3-540-49253-4_23","volume-title":"Lectures on Petri Nets I: Basic Models","author":"M. Silva","year":"1998","unstructured":"M. Silva, E. Teruel, and J. M. Colom. Linear Algebraic and Linear Programming Techniques for Analysis of Place\/Transition Net Systems. In W. Reisig and G. Rozenberg, editors. Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, LNCS 1491, pages 308\u2013309. Springer, 1998."},{"key":"28_CR26","unstructured":"D. Zampuni\u00e9ris, and B. Le Charlier. Efficient Handling of Large Sets of Tuples with Sharing Trees. In Proceedings of the Data Compressions Conference (DCC\u201995), 1995."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T10:27:27Z","timestamp":1739874447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}