{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:58:38Z","timestamp":1725861518665},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319426334"},{"type":"electronic","value":"9783319426341"}],"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-42634-1_49","type":"book-chapter","created":{"date-parts":[[2016,7,19]],"date-time":"2016-07-19T15:50:21Z","timestamp":1468943421000},"page":"611-622","source":"Crossref","is-referenced-by-count":1,"title":["Satisfiability of Linear Time Mu-Calculus on Finite Traces"],"prefix":"10.1007","author":[{"given":"Yao","family":"Liu","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":"Bin","family":"Cui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,20]]},"reference":[{"issue":"1\u20132","key":"49_CR1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1018985923441","volume":"22","author":"F Bacchus","year":"1998","unstructured":"Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Ann. Math. Artif. Intell. 22(1\u20132), 5\u201327 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"key":"49_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-51803-7_22","volume-title":"Temporal Logic in Specification","author":"B Banieqbal","year":"1989","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62\u201374. Springer, Heidelberg (1989)"},{"key":"49_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986, pp. 173\u2013183. ACM Press, New York (1986)","DOI":"10.1145\/512644.512660"},{"key":"49_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-61440-0_120","volume-title":"Automata, Languages and Programming","author":"JC Bradfield","year":"1996","unstructured":"Bradfield, J.C., Esparza, J., Mader, A.: An effective tableau system for the linear time $$\\mu $$ -calculus. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 98\u2013109. Springer, Heidelberg (1996)"},{"issue":"2","key":"49_CR5","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1093\/jigpal\/jzu030","volume":"23","author":"F Bruse","year":"2015","unstructured":"Bruse, F., Friedmann, O., Lange, M.: On guarded transformation in the modal $$\\mu $$ -calculus. Logic J. IGPL 23(2), 194\u2013216 (2015)","journal-title":"Logic J. IGPL"},{"key":"49_CR6","first-page":"593","volume-title":"KR 2002","author":"D Calvanese","year":"2002","unstructured":"Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about actions and planning in LTL action theories. In: Fensel, D., Giunchiglia, F., McGuinness, D.L., Williams, M.A. (eds.) KR 2002, pp. 593\u2013602. Morgan Kaufmann, San Francisco (2002)"},{"key":"49_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"49_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/11944836_26","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"C Dax","year":"2006","unstructured":"Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time $$\\mu $$ -calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273\u2013284. Springer, Heidelberg (2006)"},{"key":"49_CR9","series-title":"LNCS","first-page":"226","volume-title":"ECP 1999","author":"G Giacomo De","year":"2000","unstructured":"De Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning for temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 226\u2013238. Springer, Heidelberg (2000)"},{"key":"49_CR10","first-page":"854","volume-title":"IJCAI 2013","author":"G Giacomo De","year":"2013","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI 2013, pp. 854\u2013860. AAAI Press, Palo Alto (2013)"},{"key":"49_CR11","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle upon Tyne (1996)"},{"key":"49_CR12","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2006","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2006)"},{"key":"49_CR13","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169\u2013190 (2014)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"49_CR14","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.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43\u201378 (2008)","journal-title":"Acta Informatica"},{"key":"49_CR15","series-title":"LNCS","first-page":"169","volume-title":"ICALP 1980","author":"EA Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"issue":"2","key":"49_CR16","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"49_CR17","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-1-4471-3078-9_13","volume-title":"Proceedings of the International Workshop on Structures in Concurrency Theory","author":"R Kaivola","year":"1995","unstructured":"Kaivola, R.: A simple decision method for the linear time mu-calculus. In: Desel, J. (ed.) Proceedings of the International Workshop on Structures in Concurrency Theory, pp. 190\u2013204. Springer, London (1995)"},{"issue":"3","key":"49_CR18","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"49_CR19","volume-title":"IJCAI 2016","author":"Y Liu","year":"2016","unstructured":"Liu, Y., Duan, Z., Tian, C.: A decision procedure for a fragment of linear time mu-calculus. In: Kambhampati, S. (ed.) IJCAI 2016. AAAI Press, Palo Alto (2016)"},{"key":"49_CR20","first-page":"2003","volume-title":"IJCAI 2011","author":"F Patrizi","year":"2011","unstructured":"Patrizi, F., Lipoveztky, N., De Giacomo, G., Geffner, H.: Computing infinite plans for LTL goals using a classical planner. In: Walsh, T. (ed.) IJCAI 2011, pp. 2003\u20132008. AAAI Press, Palo Alto (2011)"},{"key":"49_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE Press, New York (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"49_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-52148-8_14","volume-title":"Automatic Verification Methods for Finite State Systems","author":"C Stirling","year":"1990","unstructured":"Stirling, C., Walker, D.: CCS, liveness, and local model checking in the linear time mu-calculus. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 166\u2013178. Springer, Heidelberg (1990)"},{"key":"49_CR23","series-title":"LNCS","first-page":"465","volume-title":"ICALP 1984","author":"RS Streett","year":"1984","unstructured":"Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 465\u2013472. Springer, Heidelberg (1984)"},{"key":"49_CR24","first-page":"1696","volume-title":"IJCAI 2015","author":"J Torres","year":"2015","unstructured":"Torres, J., Baier, J.A.: Polynomial-time reformulations of LTL temporally extended goals into final-state goals. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, pp. 1696\u20131703. AAAI Press, Palo Alto (2015)"},{"key":"49_CR25","first-page":"250","volume-title":"POPL 1988","author":"MY Vardi","year":"1988","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) POPL 1988, pp. 250\u2013259. ACM Press, New York (1988)"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-42634-1_49","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T18:44:22Z","timestamp":1498329862000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-42634-1_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319426334","9783319426341"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-42634-1_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}