{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:29:34Z","timestamp":1743110974427,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676935"},{"type":"electronic","value":"9783540449881"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44988-4_9","type":"book-chapter","created":{"date-parts":[[2007,7,31]],"date-time":"2007-07-31T21:38:07Z","timestamp":1185917887000},"page":"123-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Designing a LTL Model-Checker Based on Unfolding Graphs"],"prefix":"10.1007","author":[{"given":"Jean-Michel","family":"Couvreur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Grivet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Poitrenaud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,6,9]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"Proc. of FM\u201999","author":"J.-M. Couvreur","year":"1999","unstructured":"J.-M. Couvreur. On-the-fly verification of linear temporal logic. In Proc. of FM\u201999, volume 1708 of Lecture Notes in Computer Science, pages 253\u2013271. Springer Verlag, 1999."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"J.-M. Couvreur and D. Poitrenaud. Model checking based on occurrence net graph. In Proc. of Formal Description Techniques IX, Theory, Applications and Tools, pages 380\u2013395, 1996.","DOI":"10.1007\/978-0-387-35079-0_24"},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-48745-X_22","volume-title":"Proc. of ICATPN\u201999","author":"J.-M. Couvreur","year":"1999","unstructured":"J.-M. Couvreur and D. Poitrenaud. Detection of illegal behaviours based on unfoldings. In Proc. of ICATPN\u201999, volume 1639 of Lecture Notes in Computer Science, pages 364\u2013383. Springer Verlag, 1999."},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/BF01463946","volume":"28","author":"J. Engelfriet","year":"1991","unstructured":"J. Engelfriet. Branching processes of Petri nets. Acta Informatica, 28:575\u2013591, 1991.","journal-title":"Acta Informatica"},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1007\/3-540-56610-4_93","volume-title":"Proc. of TAPSOFT\u201993","author":"J. Esparza","year":"1993","unstructured":"J. Esparza. Model checking using net unfoldings. In Proc. of TAPSOFT\u201993, volume 668 of Lecture Notes in Computer Science, pages 613\u2013628. Springer Verlag, 1993."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-48320-9_2","volume-title":"Proceedings of CONCUR\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and S. R\u00f6mer. An unfolding algorithm for synchronous products of transition system. In Proceedings of CONCUR\u201999, number 1664 in LNCS, pages 2\u201320. Springer, 1999."},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61042-1_40","volume-title":"Proc. of TACAS\u201996","author":"J. Esparza","year":"1996","unstructured":"J. Esparza, S. R\u00f6mer, and W. Vogler. An improvement of McMillan\u2019s unfolding algorithm. In Proc. of TACAS\u201996, volume 1055 of Lecture Notes in Computer Science, pages 87\u2013106. Springer Verlag, 1996."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems","author":"P. Godefroid","year":"1996","unstructured":"P. Godefroid. Partial-order methods for the verification of concurrent systems. volume 1032 of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"key":"9_CR11","unstructured":"P. Godefroid and G. J. Holzmann. On the verification of temporal properties. In Proc. 13th Int. Conf on Protocol Specification, Testing, and Verification, INWG\/IFIP, pages 109\u2013124, Liege, Belgium, May 1993."},{"key":"9_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G. J. Holzmann","year":"1991","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In The Spin Verification System, pages 23\u201332. American Mathematical Society, 1996. Proc. of the Second Spin Workshop.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-61363-3_19","volume-title":"Proc. of ICATPN\u201996","author":"A. Kondratyev","year":"1996","unstructured":"A. Kondratyev, M. Kishinevsky, A. Taubin, and S. Ten. A structural approach for the analysis of Petri nets by reduced unfolding. In Proc. of ICATPN\u201996, volume 1091 of Lecture Notes in Computer Science, pages 346\u2013365. Springer Verlag, 1996."},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-48683-6_18","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification, Italy","author":"R. Langerak","year":"1999","unstructured":"R. Langerak and E. Brinksma. A complete finite prefix for process algebra. In Proceedings of the 11th International Conference on Computer Aided Verification, Italy, number 1633 in LNCS, pages 184\u2013195. Springer, 1999."},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Proc. of the 4thConference on Computer Aided Verification","author":"K.L. McMillan","year":"1992","unstructured":"K.L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. of the 4th\n Conference on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 164\u2013175. Springer Verlag, 1992."},{"key":"9_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-63166-6_35","volume-title":"Proc. of the 9thConference on Computer Aided Verification","author":"S. Melzer","year":"1997","unstructured":"S. Melzer and S. R\u00f6mer. Deadlock checking using net unfoldings. In Proc. of the 9th\n Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 352\u2013363. Springer Verlag, 1997."},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M. Nielsen","year":"1981","unstructured":"M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, events structures and domains, part I. Theoretical Computer Science, 13(1):85\u2013108, 1981.","journal-title":"Theoretical Computer Science"},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Proc. on the 5thConference on Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"D. Peled. All from one, one for all: on model checking using representatives. In Proc. on the 5th\n Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 409\u2013423. Springer Verlag, 1993."},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Doron Peled and Thomas Wilke. Stutter-invariant temporal properties are expressible without the nexttime operator. Information Processing Letters, 63:243\u2013246, 1997.","journal-title":"Information Processing Letters"},{"key":"9_CR21","volume-title":"Graphes de Processus Arborescents pour la V\u00e9rification de Propri\u00e9t\u00e9s","author":"D. Poitrenaud","year":"1996","unstructured":"D. Poitrenaud. Graphes de Processus Arborescents pour la V\u00e9rification de Propri\u00e9t\u00e9s. Th\u00e8se de doctorat, Universit\u00e9 P. et M. Curie, Paris, France, 1996."},{"issue":"3","key":"9_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal of the Association for Computing Machinery, 32(3):733\u2013749, July 1985.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"9_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets","author":"A. Valmari","year":"1991","unstructured":"A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, volume 483 of Lecture Notes in Computer Science, pages 491\u2013515. Springer Verlag, 1991."},{"key":"9_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Proc. of the 5thConference on Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"A. Valmari. On-the-fly verification with stubborn sets. In Proc. of the 5th\n Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 397\u2013408. Springer Verlag, 1993."},{"key":"9_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-55676-1_25","volume-title":"Advances in Petri Nets","author":"K. Varpaaniemi","year":"1992","unstructured":"K. Varpaaniemi and M. Rauhamaa. The stubborn set method in practice. In Advances in Petri Nets, volume 616 of Lecture Notes in Computer Science, pages 389\u2013393. Springer Verlag, 1992."},{"key":"9_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Proc. on the 10thConference on Computer Aided Verification","author":"F. Wallner","year":"1998","unstructured":"F. Wallner. Model checking LTL using net unfolding. In Proc. on the 10th\n Conference on Computer Aided Verification, Lecture Notes in Computer Science. Springer Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets 2000"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44988-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T01:13:39Z","timestamp":1635124419000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44988-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676935","9783540449881"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-44988-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"9 June 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}