{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T05:08:10Z","timestamp":1747976890910,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_18","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"216-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Decidability and Expressiveness of Recursive Weighted Logic"],"prefix":"10.1007","author":[{"given":"Kim Guldstrand","family":"Larsen","sequence":"first","affiliation":[]},{"given":"Radu","family":"Mardare","sequence":"additional","affiliation":[]},{"given":"Bingtian","family":"Xue","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"key":"18_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling, Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49\u201362. Springer, Heidelberg (2001)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147\u2013161. Springer, Heidelberg (2001)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-56496-9_32","volume-title":"Computer Aided Verification","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 410\u2013422. Springer, Heidelberg (1993)"},{"issue":"2","key":"18_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Meth. Syst. Design 2(2), 121\u2013147 (1993)","journal-title":"Form. Meth. Syst. Design"},{"volume-title":"Handbook of Weighted Automata","year":"2009","key":"18_CR8","unstructured":"Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009)"},{"key":"18_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0456-4_2","volume-title":"Dynamic Logic","author":"D Harel","year":"2001","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, Cambridge (2001)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"Automata, Languages and Programming","author":"M Hennessy","year":"1980","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299\u2013309. Springer, Heidelberg (1980)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: LICS, pp. 394\u2013406 (1992)","DOI":"10.1109\/LICS.1992.185551"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/BFb0012782","volume-title":"ICALP","author":"D Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. Lecture Notes in Computer Science, vol. 140, pp. 348\u2013359. Springer, Heidelberg (1982)"},{"issue":"2&3","key":"18_CR13","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265\u2013288 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"Mathematical Foundations of Computer Science 1995","author":"F Laroussinie","year":"1995","unstructured":"Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic - and back. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529\u2013539. Springer, Heidelberg (1995)"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.tcs.2014.03.007","volume":"546","author":"KG Larsen","year":"2013","unstructured":"Larsen, K.G., Mardare, R.: Complete proof system for weighted modal logic. Theor. Comput. Sci. 546, 164\u2013175 (2013)","journal-title":"Theor. Comput. Sci."},{"volume-title":"Advanced Topics in Bisimulation and Coinduction","year":"2011","key":"18_CR16","unstructured":"Sangiorgi, D., Rutten, J. (eds.): Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)"},{"issue":"1","key":"18_CR17","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1093\/jigpal\/7.1.103","volume":"7","author":"C Stirling","year":"1999","unstructured":"Stirling, C.: Bisimulation, modal logic and model checking games. Log. J. IGPL 7(1), 103\u2013124 (1999)","journal-title":"Log. J. IGPL"},{"issue":"2","key":"18_CR18","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"issue":"1\u20132","key":"18_CR19","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\u20132), 142\u2013182 (2000)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T18:24:21Z","timestamp":1747938261000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}