{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,19]],"date-time":"2023-09-19T05:01:35Z","timestamp":1695099695160},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,2,27]],"date-time":"2007-02-27T00:00:00Z","timestamp":1172534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transf"],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1007\/s10009-007-0030-5","type":"journal-article","created":{"date-parts":[[2007,2,26]],"date-time":"2007-02-26T04:59:09Z","timestamp":1172465949000},"page":"161-166","source":"Crossref","is-referenced-by-count":4,"title":["A negative result on depth-first net unfoldings"],"prefix":"10.1007","volume":"10","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Pradeep","family":"Kanade","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,2,27]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: Verifying finite-state graph grammars: an unfolding-based approach. In: Proceedings of CONCUR \u201904, LNCS 3170, pp. 83\u201398 (2004)","DOI":"10.1007\/978-3-540-28644-8_6"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Couvreur, J.-M., Grivet, S., Poitrenaud, D.: Unfolding of products of symmetrical Petri nets. In: Proceedings of ICATPN\u201901, LNCS 2075. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45740-2_9"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Couvreur, J.-M., Grivet, S., Poitrenaud, D.: Designing an LTL model-checker based on unfolding graphs. In: Proceedings of ICATPN 2000, LNCS 1825. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-44988-4_9"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Esparza, J., Heljanko, K.: A new unfolding approach to LTL model checking. In: Proceedings of ICALP\u201900, LNCS 1853, pp. 475\u2013486. Springer, Heidelberg, July (2000)","DOI":"10.1007\/3-540-45022-X_40"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Proceedings of SPIN\u201901, LNCS 2057, pp. 37\u201356. Springer, Heidelberg, May (2001)","DOI":"10.1007\/3-540-45139-0_4"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., R\u00f6mer, S.: An unfolding algorithm for synchronous products of transition systems. In: Proceedings of CONCUR\u201999, LNCS 1664, pp. 2\u201320. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48320-9_2"},{"key":"30_CR7","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J. Esparza","year":"2002","unstructured":"Esparza J., R\u00f6mer S. and Vogler W. (2002). An improvement of McMillan\u2019s unfolding algorithm. Form. Methods Syst. Des. 20: 285\u2013310","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"30_CR8","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s00236-003-0122-y","volume":"40","author":"V. Khomenko","year":"2003","unstructured":"Khomenko V., Koutny M. and Vogler W. (2003). Canonical prefixes of Petri net unfoldings. Acta. Inform. 40(2): 95\u2013118","journal-title":"Acta. Inform."},{"issue":"2","key":"30_CR9","first-page":"221","volume":"62","author":"V. Khomenko","year":"2004","unstructured":"Khomenko V., Koutny M. and Yakovlev A. (2004). Detecting state encoding conflicts in STG unfoldings using SAT. Fundamenta Informaticae 62(2): 221\u2013241","journal-title":"Fundamenta Informaticae"},{"key":"30_CR10","unstructured":"Khomenko, V., Koutny, M., Yakovlev, A.: Logic synthesis for asynchronous circuits based on Petri net unfoldings and incremental SAT. In: Proceedings of ACSD\u201904. IEEE (2004)"},{"key":"30_CR11","unstructured":"McMillan, K.L.: Private communication"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Proceedings of CAV\u201992, LNCS 663. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56496-9_14"},{"issue":"1","key":"30_CR13","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"K.L. McMillan","year":"1995","unstructured":"McMillan K.L. (1995). A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1): 45\u201365","journal-title":"Form. Methods Syst. Des."},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Trace theoretic verification of asynchronous circuits using unfoldings. In: Proceedings of CAV\u201995, LNCS 939. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60045-0_50"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Melzer, S., R\u00f6mer, S.: Deadlock checking using net unfoldings. In: Proceedings of CAV\u201997, LNCS 1254 (1997)","DOI":"10.1007\/3-540-63166-6_35"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Vogler,W., Semenov, A.L., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Proceedings of CONCUR \u201998, LNCS 1466. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0055644"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0030-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-007-0030-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0030-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:22Z","timestamp":1559100322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-007-0030-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,27]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["30"],"URL":"https:\/\/doi.org\/10.1007\/s10009-007-0030-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2,27]]}}}