{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,15]],"date-time":"2026-09-15T03:30:44Z","timestamp":1789443044042,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540672821","type":"print"},{"value":"9783540464198","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_29","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"426-441","source":"Crossref","is-referenced-by-count":18,"title":["Symbolic Representation of Upward-Closed Sets"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Fran\u00e7cois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. \u010cer\u0101ns, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-state Systems. In Proceedings of the 11th Annual. Symposium on Logic in Computer Science (LICS\u201996), pages 313\u2013321. IEEE Computer Society Press, 1996. 426, 427, 428, 436, 437, 438","DOI":"10.1109\/LICS.1996.561359"},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/BFb0028760","volume-title":"Proceedings of the 10th Conference on Computer Aided Verification (CAV\u201998)","author":"P. A. Abdulla","year":"1998","unstructured":"P. A. Abdulla, B. Jonsson, M. Kindahl, and D. Peled. A General Approach to Partial Order Reductions in Symbolic Verification. In Proceedings of the 10th Conference on Computer Aided Verification (CAV\u201998), volume 1427 of LNCS, pages 379\u2013390. Springer, 1998. 426, 438"},{"key":"29_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Proceedings of the 11th Conference on Computer Aided Verification (CAV\u201999)","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 Proceedings of the 11th Conference on Computer Aided Verification (CAV\u201999), volume 1633 of LNCS, pages 341\u2013353. Springer 1999. 438"},{"key":"29_CR4","series-title":"Lect Notes Comput Sci","first-page":"88","volume-title":"Proceedings of the 10th International Conference on Computer Aided Verification (CAV\u201998)","author":"B. Boigelot","year":"1998","unstructured":"B. Boigelot, P. Wolper. Verifying systems with infinite but regular state space. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV\u201998), volume 1427 of LNCS, pages 88\u201397. Springer, 1998. 426"},{"key":"29_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"Proceedings of the 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201999)","author":"A. Bouajjani","year":"1999","unstructured":"A. Bouajjani and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proceedings of the 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201999), volume 1563 of LNCS, pages 323\u2013333. Springer, 1999. 426"},{"issue":"8","key":"29_CR6","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transaction on Computers, C-35(8):667\u2013691, August, 1986. 437","journal-title":"IEEE Transaction on Computers"},{"key":"29_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Proc. 9th Conf. on Computer Aided Verification (CAV\u201997)","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics. In Proc. 9th Conf. on Computer Aided Verification (CAV\u201997), LNCS 1254, pages 400\u2013411. Springer-Verlag, 1997. 427, 437"},{"key":"29_CR8","unstructured":"BCB+90._J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pages 428\u2013439. IEEE Computer Society Press, 1990. 426, 427"},{"key":"29_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-58201-0_56","volume-title":"Proceedings of the International Conferences on Automata and Languages for Programming (ICALP 94)","author":"K. \u010cer\u0101ns","year":"1994","unstructured":"K. \u010cer\u0101ns. Deciding Properties of Integral Relational Automata. In Proceedings of the International Conferences on Automata and Languages for Programming (ICALP 94), volume 820 of LNCS, pages 35\u201346. Springer, 1994. 426"},{"key":"29_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-58152-9_11","volume-title":"Proceedings of the 15th Int. Conf. on Application and Theory of Petri Nets 1994","author":"G. Ciardo","year":"1994","unstructured":"G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In Proceedings of the 15th Int. Conf. on Application and Theory of Petri Nets 1994, LNCS 815, pages 179\u2013198. Springer-Verlag, 1994. 426"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"E. Clarke, M. Fujita, and X. Zhao. Multi-terminal Binary Decision Diagrams and Hybrid Decision Diagrams. In Representations of Discrete Functions, pages 93\u2013108. Kluwer Academic Publishers, 1996. 437","DOI":"10.1007\/978-1-4613-1385-4_4"},{"key":"29_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL\u201999)","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL\u201999), volume 1683 of LNCS, pag. 50\u201366. Springer, 1999. 426, 427, 436, 437"},{"key":"29_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Proc. 5th Int. Con. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski, Model Checking in CLP. In W. R. Cleaveland, editor, Proc. 5th Int. Con. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)., LNCS 1579, pages 223\u2013239. Springer-Verlag, 1999."},{"key":"29_CR14","unstructured":"G. Delzanno and J. F. Raskin. Symbolic Representation of Upward-Closed Sets. Technical report MPI-I-1999-2-007, Max-Planck-Institut f\u00fcr Informatik, November 1999. Available on the web at http:\/\/www.mpisb.mpg.de\/units\/ag2\/ . 428, 437"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS\u2019 98), pages 70\u201380. IEEE Computer Society Press, 1998. 426","DOI":"10.1109\/LICS.1998.705644"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS\u201999), pages 352\u2013359. IEEE Computer Society Press, 1999. 426","DOI":"10.1109\/LICS.1999.782630"},{"issue":"2","key":"29_CR17","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and Covering of Infinite Reachability Trees. Information and Computation 89(2), pages 144\u2013179. Academic Press, 1990. 426","journal-title":"Information and Computation"},{"key":"29_CR18","unstructured":"A. Finkel and P. Schnoebelen. Well-structured Transition Systems Everywhere! Theoretical Computer Science, 1999. To appear. 426, 427, 428"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"F. Gagnon, J.-Ch. Gr\u00e9goire, and D. Zampuni\u00e9ris. Sharing Trees for \u2018On-the-fly\u2019 Verification. In Proceedings of the International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201995), 1995. 437","DOI":"10.1007\/978-0-387-34945-9_30"},{"key":"29_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/3-540-63166-6_43","volume-title":"Proceedings of the 9th Conference on Computer Aided Verification (CAV\u201997)","author":"B. Grahlmann","year":"1997","unstructured":"B. Grahlmann. The PEP Tool. In Proceedings of the 9th Conference on Computer Aided Verification (CAV\u201997), volume 1254 of LNCS, pages 440\u2013443. Springer, 1997. 438"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"M. R. Henzinger, T. A. Henzinger, P. K. Kopke. Computing Simulations on Finite and Infinite Graphs. In Proceedings of the 36th Annual IEEE Symposium on Foundations of Computer Science (FOCS\u201995), pages 453\u2013462. IEEE Society Press, 1995. 434","DOI":"10.1109\/SFCS.1995.492576"},{"key":"29_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proceedings of the 9th Conference on Computer Aided Verification (CAV\u201997)","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 Proceedings of the 9th Conference on Computer Aided Verification (CAV\u201997), volume 1254 of LNCS, pages 460\u2013463. Springer, 1997. 427"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"29_CR24","volume-title":"Finite and Infinite Machines","author":"N. M. Minsky","year":"1967","unstructured":"N. M. Minsky. Finite and Infinite Machines. Prentice Hall, Englewood Cliffs, N.Y., 1967. 426"},{"key":"29_CR25","unstructured":"SKM+90._A. Srinivasan, T. Kam, S. Malik, and R. K. Brayton. Algorithms for Discrete Functions Manipulation. In Proceedings of the IEEE International. Conference on Computer-Aided Design (ICCAD\u201990), 1990. 437"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"K. Strehl, L. Thiele. Interval Diagram Techniques For Symbolic Model Checking of Petri Nets. In Proceedings of the Design, Automation and Test in Europe Conference (DATE\u201999), pages 756\u2013757, 1999. 438","DOI":"10.1145\/307418.307452"},{"key":"29_CR27","unstructured":"E. Teruel. Structure Theory of Weighted Place\/Transition Net Systems: The Equal Conflict Hiatus. Ph.D. Thesis, University of Zaragoza, 1994. 426, 427, 436"},{"key":"29_CR28","unstructured":"G. Wimmel. A BDD-based Model Checker for the PEP Tool. Technical Report, University of Newcastle Upon Tyne, 1997. 438"},{"key":"29_CR29","volume-title":"The Sharing Tree Data Structure: Theory and Applications in Formal Verification","author":"D. Zampuni\u00e9ris","year":"1997","unstructured":"D. Zampuni\u00e9ris. The Sharing Tree Data Structure: Theory and Applications in Formal Verification. PhD Thesis. Facult\u00e9s Universitaires Notre-Dame de la Paix, Namur, Belgium, May 1997. 427, 436, 437"},{"key":"29_CR30","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. 427, 429, 430, 431, 432, 435"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:00:31Z","timestamp":1737352831000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}