{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:19Z","timestamp":1760202559211},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421245"},{"type":"electronic","value":"9783540451396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_4","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"37-56","source":"Crossref","is-referenced-by-count":26,"title":["Implementing LTL model checking with net unfoldings"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"4_CR1","series-title":"Technical report","volume-title":"Evaluating deadlock detection methods for concurrent software","author":"J. C. Corbett","year":"1995","unstructured":"J. C. Corbett. Evaluating deadlock detection methods for concurrent software. Technical report, Department of Information and Computer Science, University of Hawaii at Manoa, 1995."},{"key":"4_CR2","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":"4_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/3-540-45022-X_40","volume-title":"Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP\u20192000)","author":"J. Esparza","year":"2000","unstructured":"J. Esparza and K. Heljanko. A new unfolding approach to LTL model checking. In Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP\u20192000), pages 475\u2013486, July 2000. LNCS 1853."},{"key":"4_CR4","series-title":"Research Report","volume-title":"Implementing LTL model checking with net unfoldings","author":"J. Esparza","year":"2001","unstructured":"J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. Research Report A68, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2001. Available at \u2329 http:\/\/www.tcs.hut.fi\/Publications\/reports\/A68abstract.htm \u232a."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-48320-9_2","volume-title":"Proceedings of the 10th International Conference on Concurrency Theory (Concur\u201999)","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and S. R\u00f6mer. An unfolding algorithm for synchronous products of transition systems. In Proceedings of the 10th International Conference on Concurrency Theory (Concur\u201999), pages 2\u201320, 1999. LNCS 1664."},{"key":"4_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61042-1_40","volume-title":"Proceedings of 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996)","author":"J. Esparza","year":"1996","unstructured":"J. Esparza, S. R\u00f6mer, and W. Vogler. An improvement of McMillan\u2019s unfolding algorithm. In Proceedings of 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), pages 87\u2013106, 1996. LNCS 1055."},{"key":"4_CR7","series-title":"Informatik-Bericht","first-page":"255","volume-title":"Proceeding of the Workshop Concurrency, Specification & Programming 2000","author":"J. Esparza","year":"2000","unstructured":"J. Esparza and C. Schr\u00f6ter. Reachability analysis using net unfoldings. In Proceeding of the Workshop Concurrency, Specification & Programming 2000, volume II of Informatik-Bericht 140, pages 255\u2013270. Humboldt-Universit\u00e4t zu Berlin, 2000."},{"key":"4_CR8","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 Proceedings of 15th Workshop Protocol Specification, Testing, and Verification, pages 3\u201318, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"4_CR9","series-title":"Technical Report Technical Report","volume-title":"Petri net based qualitative analysis-A case study","author":"M. Heiner","year":"1995","unstructured":"M. Heiner and P. Deussen. Petri net based qualitative analysis-A case study. Technical Report Technical Report I-08\/1995, Brandenburg Technische Universit\u00e4t Cottbus, Cottbus, Germany, December 1995."},{"key":"4_CR10","series-title":"Research Report","volume-title":"Deadlock and reachability checking with finite complete prexes","author":"K. Heljanko","year":"1999","unstructured":"K. Heljanko. Deadlock and reachability checking with finite complete prexes. Research Report A56, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 1999. Licentiate\u2019s Thesis. Available at \u2329 http:\/\/www.tcs.hut.fi\/Publications\/reports\/A56abstract.htm \u232a."},{"issue":"3","key":"4_CR11","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/FI-1999-37304","volume":"37","author":"K. Heljanko","year":"1999","unstructured":"K. Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. Fundamenta Informaticae, 37(3):247\u2013268, 1999.","journal-title":"Fundamenta Informaticae"},{"issue":"5","key":"4_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-58867-1","volume-title":"Formal Development of Reactive Systems: Case Study Production Cell","author":"C. Lewerentz","year":"1995","unstructured":"C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. Springer-Verlag, 1995. LNCS 891."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/3-540-63166-6_35","volume-title":"Proceedings of 9th International Conference on Computer-Aided Verification (CAV\u2019 97)","author":"S. Melzer","year":"1997","unstructured":"S. Melzer and S. R\u00f6mer. Deadlock checking using net unfoldings. In Proceedings of 9th International Conference on Computer-Aided Verification (CAV\u2019 97), pages 352\u2013363, 1997. LNCS 1254."},{"key":"4_CR16","series-title":"Technical Report","volume-title":"Verification of fault tolerant algorithms using PEP","author":"S. Merkel","year":"1997","unstructured":"S. Merkel. Verification of fault tolerant algorithms using PEP. Technical Report TUM-19734, SFB-Bericht Nr. 342\/23\/97 A, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany, 1997."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"W. Reisig. Petri Nets, An Introduction. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"4_CR18","series-title":"PhD thesis","volume-title":"Extending and Implementing the Stable Model Semantics","author":"P. Simons","year":"2000","unstructured":"P. Simons. Extending and Implementing the Stable Model Semantics. PhD thesis, Helsinki University of Technology, Laboratory for Theoretical Computer Science, April 2000. Also available on the Internet at \u2329 http:\/\/www.tcs.hut.fi\/Publications\/reports\/A58abstract.htm \u232a."},{"key":"4_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Proceeding of 5th International Conference on Computer Aided Verification (CAV\u201993)","author":"A. Valmari","year":"1993","unstructured":"A. Valmari. On-the-fly verification with stubborn sets. In Proceeding of 5th International Conference on Computer Aided Verification (CAV\u201993), pages 397\u2013408, 1993. LNCS 697."},{"key":"4_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M. Y. Vardi","year":"1996","unstructured":"M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, pages 238\u2013265, 1996. LNCS 1043."},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-63166-6_51","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV\u201997)","author":"K. Varpaaniemi","year":"1997","unstructured":"K. Varpaaniemi, K. Heljanko, and J. Lilius. PROD 3.2-An advanced tool for efficient reachability analysis. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV\u201997), pages 472\u2013475, 1997. LNCS 1254."},{"key":"4_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BFb0028746","volume-title":"Proceeding of 10th International Conference on Computer Aided Verification (CAV\u201998)","author":"F. Wallner","year":"1998","unstructured":"F. Wallner. Model checking LTL using net unfoldings. In Proceeding of 10th International Conference on Computer Aided Verification (CAV\u201998), pages 207\u2013218, 1998. LNCS 1427."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T19:38:45Z","timestamp":1587843525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}