{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T23:39:06Z","timestamp":1648942746391},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,3,7]],"date-time":"2013-03-07T00:00:00Z","timestamp":1362614400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comb Optim"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10878-013-9601-4","type":"journal-article","created":{"date-parts":[[2013,3,6]],"date-time":"2013-03-06T05:35:12Z","timestamp":1362548112000},"page":"406-417","source":"Crossref","is-referenced-by-count":1,"title":["Transformation from PLTL to automata via NFGs"],"prefix":"10.1007","volume":"29","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,3,7]]},"reference":[{"key":"9601_CR1","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"JA Brzozowski","year":"1980","unstructured":"Brzozowski JA, Leiss E (1980) Finite automata, and sequential networks. Theor Comput Sci 10:19\u201335","journal-title":"Theor Comput Sci"},{"issue":"1","key":"9601_CR2","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra AK, Kozen DC, Stockmeyer LJ (1981) Alternation. J Assoc Comput Mach 28(1):114\u2013133","journal-title":"J Assoc Comput Mach"},{"key":"9601_CR3","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Hamaguchi K (1994) Another look at LTL model checking. CAV94, Springer, pp 415\u2013427","DOI":"10.1007\/3-540-58179-0_72"},{"key":"9601_CR4","doi-asserted-by":"crossref","unstructured":"Daniele N, Guinchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. CAV99, LNCS 1633, Springer, pp 249\u2013260","DOI":"10.1007\/3-540-48683-6_23"},{"key":"9601_CR5","unstructured":"Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D thesis, University of Newcastle Upon Tyne"},{"issue":"1","key":"9601_CR6","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan Z, Tian C, Zhang L (2008) A decision procedure for propositional projection temporal logic with infinite models. Acta Inform 45(1):43\u201378","journal-title":"Acta Inform"},{"key":"9601_CR7","doi-asserted-by":"crossref","unstructured":"Emerson AE (1990) Temporal and modal logic, In: Jan van Leeuwen (ed) Handbook of theoretical computer science, volume B: Formal methods and semantics, pp 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"9601_CR8","doi-asserted-by":"crossref","unstructured":"Etessami K, Holzmann GJ (2000) Optimizing B\u00fcchi automata. In: Proceedings of 11th international conference on concurrency theory, LNCS 1877, Springer, pp 153\u2013167","DOI":"10.1007\/3-540-44618-4_13"},{"key":"9601_CR9","unstructured":"Fritz C (2003) Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating bchi automata. ICIAA03, LNCS 2759, Springer, pp 35\u201348"},{"key":"9601_CR10","doi-asserted-by":"crossref","unstructured":"Fritz C (2005) Concepts of automata construction from LTL. In: Proceedings of ICLPAIR 2005, LNCS 3835, Springer, pp 728\u2013742","DOI":"10.1007\/11591191_50"},{"key":"9601_CR11","unstructured":"Gerth R, Peled D, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, Vancouver, pp 3\u201318"},{"key":"9601_CR12","unstructured":"Katoen JP (1999) Concepts, algorithms, and tools for model checking. Lecture notes of the course mechanised validation of parallel systems"},{"key":"9601_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of 18th symposium on foundations of computer science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"9601_CR14","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logics. J ACM 32(3):733\u2013749","journal-title":"J ACM"},{"key":"9601_CR15","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. CAV00, Lecture notes in computer science, vol 1855. Springer, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"9601_CR16","doi-asserted-by":"crossref","unstructured":"Thirioux X (2002) Simple and efficient translation from LTL formulas to B\u00fcchi automata. Electr Notes Theor Comput Sci 66(2):145\u2013159","DOI":"10.1016\/S1571-0661(04)80409-2"},{"issue":"1","key":"9601_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"},{"key":"9601_CR18","doi-asserted-by":"crossref","unstructured":"Vardi MY (1994) Nontraditional applications of automata theory. In: International symposium on theoretical aspects of computer software, LNCS 789, Springer, pp 575\u2013597","DOI":"10.1007\/3-540-57887-0_116"},{"key":"9601_CR19","doi-asserted-by":"crossref","unstructured":"Vardi MY (1995) Alternating automata and program verification. In: Computer science today. LNCS 1000, Springer, pp 471\u2013485","DOI":"10.1007\/BFb0015261"},{"key":"9601_CR20","doi-asserted-by":"crossref","unstructured":"Vardi MY (2007) Automata-theoretic model checking revisited. VMCAI 07. LNCS 4349. Springer, New York, pp 137\u2013150","DOI":"10.1007\/978-3-540-69738-1_10"},{"key":"9601_CR21","doi-asserted-by":"crossref","unstructured":"Wolper P, Vardi MY, Sistla AP (1983) Reasoning about infinite computation paths. In: Proceedings of 24th IEEE symposium on foundations of computer science, Tucson, pp 185\u2013194","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-013-9601-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-013-9601-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-013-9601-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T14:21:30Z","timestamp":1562768490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-013-9601-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,7]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9601"],"URL":"https:\/\/doi.org\/10.1007\/s10878-013-9601-4","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"value":"1382-6905","type":"print"},{"value":"1573-2886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,7]]}}}