{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:42:40Z","timestamp":1743007360109,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"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_6","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"76-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Present-Future Form of Linear Time $$\\mu $$-Calculus"],"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":"Bo","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,21]]},"reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","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. Theoret. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Conference Record of the 13th Annual ACM Symposium on Principles of Programming Languages, pp. 173\u2013183. ACM (1986)","DOI":"10.1145\/512644.512660"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages, pp. 250\u2013259. ACM (1988)","DOI":"10.1145\/73560.73582"},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1), 72\u201399 (1983)","journal-title":"Inf. Control"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"RS Streett","year":"1989","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput. 81(3), 249\u2013264 (1989)","journal-title":"Inf. Comput."},{"key":"6_CR6","series-title":"LNCS","first-page":"385","volume-title":"CAV 1993","author":"EA Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of $$\\mu $$-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385\u2013396. Springer, Heidelberg (1993)"},{"issue":"2","key":"6_CR7","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"6_CR8","series-title":"LNCS","doi-asserted-by":"publisher","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., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62\u201374. Springer, Heidelberg (1989)"},{"key":"6_CR9","series-title":"LNCS","first-page":"166","volume-title":"CAV 1989","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.) CAV 1989. LNCS, vol. 407, pp. 166\u2013178. Springer, Heidelberg (1990)"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C Stirling","year":"1991","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theoret. Comput. Sci. 89(1), 161\u2013177 (1991)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Kaivola, R.: A simple decision method for the linear time mu-calculus. In: Proceedings of the International Workshop on Structures in Concurrency Theory, pp. 190\u2013204. Springer (1995)","DOI":"10.1007\/978-1-4471-3078-9_13"},{"key":"6_CR12","series-title":"LNCS","first-page":"98","volume-title":"ICALP 1996","author":"J Bradfield","year":"1996","unstructured":"Bradfield, J., 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)"},{"key":"6_CR13","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":"6_CR14","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":"6_CR15","series-title":"LNCS","first-page":"521","volume-title":"TAMC 2007","author":"Z Duan","year":"2007","unstructured":"Duan, Z., Tian, C.: Decidability of propositional projection temporal logic with infinite models. In: Cai, J.-Y., Cooper, S.B., Zhu, H. (eds.) TAMC 2007. LNCS, vol. 4484, pp. 521\u2013532. Springer, Heidelberg (2007)"},{"issue":"1","key":"6_CR16","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 Inf. 45(1), 43\u201378 (2008)","journal-title":"Acta Inf."},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: Complexity of propositional projection temporal logic with star. Math. Struct. Comput. Sci. 19(1), 73\u2013100 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"6_CR18","series-title":"LNCS","first-page":"90","volume-title":"ICFEM 2010","author":"Z Duan","year":"2010","unstructured":"Duan, Z., Tian, C.: An improved decision procedure for propositional projection temporal logic. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 90\u2013105. Springer, Heidelberg (2010)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Modal and temporal logics. LFCS, Department of Computer Science, University of Edinburgh (1991)","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1999.2836","volume":"157","author":"I Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Completeness of Kozen\u2019s axiomatisation of the propositional $$\\mu $$-calculus. Inf. Comput. 157(1), 142\u2013182 (2000)","journal-title":"Inf. Comput."}],"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_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T12:00:17Z","timestamp":1716552017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_6","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"}}]}}