{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:53:01Z","timestamp":1725742381322},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396977"},{"type":"electronic","value":"9783642396984"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39698-4_16","type":"book-chapter","created":{"date-parts":[[2013,7,24]],"date-time":"2013-07-24T17:03:05Z","timestamp":1374685385000},"page":"256-270","source":"Crossref","is-referenced-by-count":4,"title":["On the Relationship between LTL Normal Forms and B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Zheng","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Guldstrand Larsen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi Automata Translation: Fast and More Deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 95\u2013109. Springer, Heidelberg (2012)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a0CAV, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"16_CR3","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata In. In: The IEEE Computer Society\u2019s 12th Annual International Symposium, pp. 76\u201383 (2004)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi Automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","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.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Li, J., Pu, G., Zhang, L., Wang, Z., He, J., Larsen, K.G.: On the Relationship between LTL Normal Forms and Buechi Automata. CoRR (2012)","DOI":"10.1007\/978-3-642-39698-4_16"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"K.Y. Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore Deterministic\u201d vs. \u201cSmaller\u201d B\u00fcchi Automata for Efficient LTL Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"issue":"1","key":"16_CR12","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT\u00a04(1), 57\u201370 (2002)","journal-title":"STTT"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An Automata-Theoretic Approach to Linear Temporal Logic. In: Banff Higher Order Workshop, pp. 238\u2013266 (1995)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"16_CR14","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS, pp. 332\u2013344 (1986)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers, 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"}],"container-title":["Lecture Notes in Computer Science","Theories of Programming and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39698-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T03:55:03Z","timestamp":1557978903000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39698-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396977","9783642396984"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39698-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}