{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:40:10Z","timestamp":1748806810076,"version":"3.41.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319312194"},{"type":"electronic","value":"9783319312200"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-31220-0_13","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T13:59:52Z","timestamp":1457791192000},"page":"179-194","source":"Crossref","is-referenced-by-count":2,"title":["LtlNfBa: Making LTL Translation More Practical"],"prefix":"10.1007","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhao","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"13_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, Tucson, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"13_CR4","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, London (1995)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575\u2013597. Springer, Heidelberg (1994)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"MY Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"13_CR8","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. 1633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"13_CR9","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. 1877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Implementation and Application of Automata","author":"C Fritz","year":"2003","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/11591191_50","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Fritz","year":"2005","unstructured":"Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 728\u2013742. Springer, Heidelberg (2005)"},{"key":"13_CR12","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. 1855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/S1571-0661(04)80409-2","volume":"66","author":"X Thirioux","year":"2002","unstructured":"Thirioux, X.: Simple and efficient translation from LTL formulas to B\u00fcchi automata. Electr. Notes Theor. Comput. Sci. 66(2), 145\u2013159 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43\u201378 (2008)","journal-title":"Acta Informatica"},{"key":"13_CR15","first-page":"995","volume-title":"Formal Models and Semantics","author":"E. Allen EMERSON","year":"1990","unstructured":"Emerson, A.E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol. B, pp. 995\u20131072 (1990)"},{"key":"13_CR16","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle Upon Tyne, May 1996"},{"key":"13_CR17","unstructured":"Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking. Lecture Notes of the Course Mechanised Validation of Parrel Systems (1999)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In CAV , LNCS 2102, pp. 53\u201365, Springer-Verlag, 2001. (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"13_CR19","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. 7214, pp. 95\u2013109. Springer, Heidelberg (2012)"},{"key":"13_CR20","doi-asserted-by":"crossref","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":"Tom\u00e1\u0161 Babiak","year":"2012","unstructured":"Babiak, T., Kretinsky, M., Rehak, V., Strejcek, J.: LTL to B\u00fcchi Automata Translation: Fast and More Deterministic. CoRR, abs\/1201.0682 (2012)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: MASCOTS 2004, pp. 76\u201383 (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"13_CR22","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. 1708, p. 253. Springer, Heidelberg (1999)"},{"issue":"13","key":"13_CR23","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1016\/j.ipl.2009.02.020","volume":"109","author":"C Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: A note on stutter-invariant PLTL. Inf. Process. Lett. 109(13), 663\u2013667 (2009)","journal-title":"Inf. Process. Lett."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Cichon, J., Czubak, A., Jasinski, A.: Minimal B\u00fcchi automata for certain classes of LTL formulas. In: DEPCOS-RELCOMEX 2009, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/DepCoS-RELCOMEX.2009.31"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-31220-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:22:14Z","timestamp":1748805734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31220-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319312194","9783319312200"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31220-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}