{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:32Z","timestamp":1751983652988},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_31","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"549-567","source":"Crossref","is-referenced-by-count":28,"title":["A Generalised Sweep-Line Method for Safety Properties"],"prefix":"10.1007","author":[{"given":"Lars Michael","family":"Kristensen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Mailund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"issue":"8","key":"31_CR1","doi-asserted-by":"publisher","first-page":"677","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 Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"31_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/3-540-45319-9_30","volume-title":"Proceedings of TACAS 2001","author":"R. Carvajal-Schiaffino","year":"2001","unstructured":"R. Carvajal-Schiaffino, G. Delzanno, and G. Chiola. Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets. In Proceedings of TACAS 2001, volume 2031 of LNCS, pages 435\u2013449. Springer-Verlag, 2001."},{"key":"31_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/3-540-63139-9_47","volume-title":"Proceedings of ICATPN\u201997","author":"S. Christensen","year":"1997","unstructured":"S. Christensen and J.B. J\u00f8rgensen. Analysis of Bang and Olufsen\u2019s BeoLink Audio\/Video System Using Coloured Petri Nets. In Proceedings of ICATPN\u201997, volume 1248 of LNCS, pages 387\u2013406. Springer-Verlag, 1997."},{"key":"31_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BFb0035390","volume-title":"Proceedings of TACAS\u201997","author":"S. Christensen","year":"1997","unstructured":"S. Christensen, J.B. J\u00f8rgensen, and L.M. Kristensen. Design\/CPN-A Computer Tool for Coloured Petri Nets. In Proceedings of TACAS\u201997, volume 1217 of LNCS, pages 209\u2013223. Springer-Verlag, 1997."},{"key":"31_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Proceedings of TACAS 2001","author":"S. Christensen","year":"2001","unstructured":"S. Christensen, L.M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Proceedings of TACAS 2001, volume 2031 of LNCS, pages 450\u2013464. Springer-Verlag, 2001."},{"issue":"1\/2","key":"31_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting Symmetries in Temporal Logic Model Checking. Formal Methods in System Design, 9(1\/2):77\u2013104, 1996.","journal-title":"Formal Methods in System Design"},{"issue":"1\/2","key":"31_CR7","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"E.A. Emerson and A.P. Sistla. Symmetry and Model Checking. Formal Methods in System Design, 9(1\/2):105\u2013131, 1996.","journal-title":"Formal Methods in System Design"},{"key":"31_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem, volume 1032 of LNCS. Springer-Verlag, 1996."},{"key":"31_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of ICATPN 2002","author":"S. Gordon","year":"2002","unstructured":"S. Gordon, L.M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol. In Proceedings of ICATPN 2002, LNCS. Springer-Verlag, 2002. To appear."},{"key":"31_CR10","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991."},{"issue":"3","key":"31_CR11","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"G.J. Holzmann. An Analysis of Bitstate Hashing. Formal Methods in System Design, 13(3):287\u2013305, 1998.","journal-title":"Formal Methods in System Design"},{"key":"31_CR12","series-title":"Lect Notes Comput Sci","first-page":"192","volume-title":"Proceedings of CAV\u201991","author":"C. Jard","year":"1991","unstructured":"C. Jard and T. Jeron. Bounded-memory Algorithms for Verification On-the-fly. In Proceedings of CAV\u201991, volume 575 of LNCS, pages 192\u2013202. Springer-Verlag, 1991."},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 1: Basic Concepts. Monographs in Theoretical Computer Science. Springer-Verlag, 1992.","DOI":"10.1007\/978-3-662-06289-0"},{"key":"31_CR14","unstructured":"K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 2: Analysis Methods. Monographs in Theoretical Computer Science. Springer-Verlag, 1994."},{"issue":"1\/2","key":"31_CR15","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00625967","volume":"9","author":"K. Jensen","year":"1996","unstructured":"K. Jensen. Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design, 9(1\/2):7\u201340, 1996.","journal-title":"Formal Methods in System Design"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3: Practical Use. iMonographs in Theoretical Computer Science. Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-60794-3"},{"issue":"3","key":"31_CR17","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1023\/A:1008775109219","volume":"14","author":"S. Katz","year":"1999","unstructured":"S. Katz and H. Miller. Saving Space by Fully Exploiting Invisible Transitions. Formal Methods in System Design, 14(3):311\u2013332, 1999.","journal-title":"Formal Methods in System Design"},{"key":"31_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-69108-1_7","volume-title":"Proceedings of ICATPN\u201998","author":"L. M. Kristensen","year":"1998","unstructured":"L. M. Kristensen and A. Valmari. Finding Stubborn Sets of Coloured Petri Nets Without Unfolding. In Proceedings of ICATPN\u201998, volume 1420 of LNCS, pages 104\u2013123. Springer-Verlag, 1998."},{"issue":"2","key":"31_CR19","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s100090050021","volume":"2","author":"L.M. Kristensen","year":"1998","unstructured":"L.M. Kristensen, S. Christensen, and K. Jensen. The Practitioner\u2019s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer, 2(2):98\u2013132, 1998.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"31_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/BFb0035380","volume-title":"Proceedings of TACAS\u201997","author":"A.N. Parashkevov","year":"1997","unstructured":"A.N. Parashkevov and J. Yantchev. Space Efficient Reachability Analysis Through Use of Pseudo-Root States. In Proceedings of TACAS\u201997, volume 1217 of LNCS, pages 50\u201364. Springer-Verlag, 1997."},{"key":"31_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Proceedings of CAV\u201993","author":"D. Peled","year":"1993","unstructured":"D. Peled. All from One, One for All: On Model Checking Using Representatives. In Proceedings of CAV\u201993, volume 697 of LNCS, pages 409\u2013423. Springer-Verlag, 1993."},{"key":"31_CR23","unstructured":"J.D. Ullman. Elements of ML Programming. Prentice-Hall, 1998."},{"key":"31_CR24","series-title":"Lect Notes Comput Sci","first-page":"156","volume-title":"Proceedings of CAV\u201990","author":"A. Valmari","year":"1990","unstructured":"A. Valmari. A Stubborn Attack on State Explosion. In Proceedings of CAV\u201990, volume 531 of LNCS, pages 156\u2013165. Springer-Verlag, 1990."},{"key":"31_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A. Valmari","year":"1998","unstructured":"A. Valmari. The State Explosion Problem. In Lectures on Petri Nets I: Basic Models, volume 1491 of LNCS, pages 429\u2013528. Springer-Verlag, 1998."},{"key":"31_CR26","unstructured":"M. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In In Proc. of IEEE Symposium on Logic in Computer Science, pages 322\u2013331, 1986."},{"key":"31_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CONCUR\u201993","author":"P. Wolper","year":"1993","unstructured":"P. Wolper and P. Godefroid. Partial Order Methods for Temporal Verification. In Proceedings of CONCUR\u201993, volume 715 of LNCS. Springer-Verlag, 1993."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,24]],"date-time":"2019-01-24T07:32:33Z","timestamp":1548315153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}