{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:16:26Z","timestamp":1746159386051,"version":"3.40.4"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319049144"},{"type":"electronic","value":"9783319049151"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-04915-1_4","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"48-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Improved Net Reductions for LTL$$\\setminus $$X Model Checking"],"prefix":"10.1007","author":[{"given":"Ya","family":"Shi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hua","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,21]]},"reference":[{"key":"4_CR1","series-title":"LNCS","first-page":"166","volume-title":"CONCUR 1990","author":"J Desel","year":"1990","unstructured":"Desel, J.: Reduction and design of well-behaved concurrent systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 166\u2013181. Springer, Heidelberg (1990)"},{"issue":"1","key":"4_CR2","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1006\/inco.1994.1080","volume":"114","author":"J Esparza","year":"1994","unstructured":"Esparza, J.: Reduction and synthesis of live and bounded free choice petri nets. Inf. Comput. 114(1), 50\u201387 (1994)","journal-title":"Inf. Comput."},{"key":"4_CR3","series-title":"LNCS","first-page":"475","volume-title":"ICALP 2000","author":"J Esparza","year":"2000","unstructured":"Esparza, J., Heljanko, K.: A new unfolding approach to LTL model checking. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 475\u2013486. Springer, Heidelberg (2000)"},{"key":"4_CR4","series-title":"LNCS","first-page":"37","volume-title":"SPIN 2001","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37\u201356. Springer, Heidelberg (2001)"},{"issue":"2","key":"4_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10009-007-0030-5","volume":"10","author":"J Esparza","year":"2008","unstructured":"Esparza, J., Kanade, P., Schwoon, S.: A negative result on depth-first net unfoldings. Softw. Tools Technol. Transfer 10(2), 161\u2013166 (2008)","journal-title":"Softw. Tools Technol. Transfer"},{"issue":"3","key":"4_CR6","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J Esparza","year":"2002","unstructured":"Esparza, J., R\u00f6mer, S., Vogler, W.: An improvement of Mcmillan\u2019s unfolding algorithm. Formal Methods Syst. Des. 20(3), 285\u2013310 (2002)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR7","series-title":"LNCS","first-page":"310","volume-title":"CHARME 2001","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Schr\u00f6ter, C.: Net reductions for LTL model-checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 310\u2013324. Springer, Heidelberg (2001)"},{"issue":"3","key":"4_CR8","first-page":"231","volume":"47","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Schr\u00f6ter, C.: Unfolding based algorithms for the reachability problem. Fundamenta Informaticae 47(3), 231\u2013245 (2001)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR9","series-title":"LNCS","first-page":"53","volume-title":"CAV 2001","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1142\/S0129626406002502","volume":"16","author":"S Haddad","year":"2006","unstructured":"Haddad, S., Pradat-Peyre, J.F.: New efficient petri nets reductions for parallel programs verification. Parallel Process. Lett. 16(1), 101\u2013116 (2006)","journal-title":"Parallel Process. Lett."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Heljanko, K.: Deadlock and reachability checking with finite complete prefixes. Research Report A56, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo (1999)","DOI":"10.1007\/3-540-44618-4_10"},{"issue":"2","key":"4_CR12","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1109\/TSMC.1987.4309041","volume":"17","author":"L Hyung","year":"1987","unstructured":"Hyung, L., Favrel, J., Baptiste, P.: Generalized petri net reduction method. IEEE Trans. Syst. Man Cybern. SMC 17(2), 297\u2013303 (1987)","journal-title":"IEEE Trans. Syst. Man Cybern. SMC"},{"key":"4_CR13","volume-title":"Concepts, Algorithms, and Tools for Model Checking","author":"JP Katoen","year":"1999","unstructured":"Katoen, J.P.: Concepts, Algorithms, and Tools for Model Checking. IMMD, Erlangen (1999)"},{"issue":"2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10703-006-0022-1","volume":"30","author":"V Khomenko","year":"2007","unstructured":"Khomenko, V., Koutny, M.: Verification of bounded petri nets using integer programming. Formal Methods Syst. Des. 30(2), 143\u2013176 (2007)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Springer, New York (1993)"},{"key":"4_CR16","series-title":"LNCS","first-page":"164","volume-title":"CAV 1992","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164\u2013177. Springer, Heidelberg (1993)"},{"key":"4_CR17","series-title":"LNCS","first-page":"352","volume-title":"CAV 1997","author":"S Melzer","year":"1997","unstructured":"Melzer, S., R\u00f6mer, S.: Deadlock checking using net unfoldings. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 352\u2013363. Springer, Heidelberg (1997)"},{"key":"4_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/BFb0027047","volume-title":"Current Trends in Concurrency","author":"A Pnueli","year":"1986","unstructured":"Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510\u2013584. Springer, Heidelberg (1986)"},{"key":"4_CR19","series-title":"LNCS","first-page":"207","volume-title":"CAV 1998","author":"F Wallner","year":"1998","unstructured":"Wallner, F.: Model checking LTL using net unforldings. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 207\u2013218. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-04915-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T22:07:28Z","timestamp":1746137248000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"21 February 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}