{"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":1760202559018},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677154"},{"type":"electronic","value":"9783540450221"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45022-x_40","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T18:57:25Z","timestamp":1194980245000},"page":"475-486","source":"Crossref","is-referenced-by-count":18,"title":["A New Unfolding Approach to LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,18]]},"reference":[{"key":"40_CR1","unstructured":"Bibliography on the net unfolding method. Available on the Internet at http:\/\/wwwbrauer.in.tum.de\/gruppen\/theorie\/pom\/pom.shtml ."},{"key":"40_CR2","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","volume":"23","author":"J. Esparza","year":"1994","unstructured":"J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151\u2013195, 1994.","journal-title":"Science of Computer Programming"},{"key":"40_CR3","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 1055."},{"key":"40_CR4","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":"40_CR5","volume-title":"Research Report A60","author":"J. Esparza","year":"2000","unstructured":"Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. Research Report A60, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, April 2000. Available at http:\/\/www.tcs.hut.fi\/pub\/reports\/A60.ps.gz ."},{"key":"40_CR6","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":"40_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/BFb0058040","volume-title":"Proceedings of 17th Foundations of Software Technology and Theoretical Computer Science Conference","author":"B. Graves","year":"1997","unstructured":"B. Graves. Computing reachability properties hidden in finite net unfoldings. In Proceedings of 17th Foundations of Software Technology and Theoretical Computer Science Conference, pages 327\u2013341, 1997. LNCS 1346."},{"key":"40_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-49059-0_17","volume-title":"Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","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. In Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), pages 240\u2013254, 1999. LNCS 1579."},{"key":"40_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-63166-6_8","volume-title":"Proceeding of 9th International Conference on Computer Aided Verification (CAV\u201997)","author":"R. Kaivola","year":"1997","unstructured":"R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In Proceeding of 9th International Conference on Computer Aided Verification (CAV\u201997), pages 48\u201359, 1997. LNCS 1254."},{"key":"40_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-48683-6_18","volume-title":"Proceeding of 11th International Conference on Computer Aided Verification (CAV\u201999)","author":"R. Langerak","year":"1999","unstructured":"R. Langerak and E. Brinksma. A complete finite prefix for process algebra. In Proceeding of 11th International Conference on Computer Aided Verification (CAV\u201999), pages 184\u2013195, 1999. LNCS 1663."},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"40_CR12","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":"40_CR13","unstructured":"P. Niebert. Personal communication, 1999."},{"issue":"1","key":"40_CR14","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and David Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161\u2013177, 1991.","journal-title":"Theoretical Computer Science"},{"key":"40_CR15","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":"40_CR16","unstructured":"F. Wallner. Model checking techniques using net unfoldings. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Germany, forthcoming."},{"key":"40_CR17","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."},{"issue":"12","key":"40_CR18","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1,2):72\u201393, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45022-X_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T07:25:35Z","timestamp":1556954735000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45022-X_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677154","9783540450221"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45022-x_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}