{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:10:08Z","timestamp":1746375008933,"version":"3.40.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319108810"},{"type":"electronic","value":"9783319108827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10882-7_27","type":"book-chapter","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T06:54:19Z","timestamp":1410418459000},"page":"460-476","source":"Crossref","is-referenced-by-count":1,"title":["A Decidable Recursive Logic for Weighted Transition Systems"],"prefix":"10.1007","author":[{"given":"Kim Guldstrand","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Mardare","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bingtian","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS, pp. 414\u2013425 (1990)","DOI":"10.1007\/3-540-54233-7_128"},{"issue":"1","key":"27_CR2","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.\u00a0104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"issue":"1","key":"27_CR3","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. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"27_CR4","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.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: modelling, specification and verification. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511814105"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Torre, S.L., Pappas, G.J.: Optimal paths in weighted timed automata. In: Benedetto and Sangiovanni-Vincentelli [BSV01], pp. 49\u201362","DOI":"10.1007\/3-540-45351-2_8"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Benedetto and Sangiovanni-Vincentelli [BSV01], pp. 147\u2013161","DOI":"10.1007\/3-540-45351-2_15"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45351-2","volume-title":"Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001","author":"M.D. Benedetto Di","year":"2001","unstructured":"Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L.: HSCC 2001. LNCS, vol.\u00a02034. Springer, Heidelberg (2001)"},{"key":"27_CR9","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: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 410\u2013422. Springer, Heidelberg (1993)"},{"issue":"2","key":"27_CR10","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. Formal Methods in System Design\u00a02(2), 121\u2013147 (1993)","journal-title":"Formal Methods in System Design"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer (2009)","DOI":"10.1007\/978-3-642-01492-5"},{"key":"27_CR12","doi-asserted-by":"publisher","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"G.E. Hughes","year":"1996","unstructured":"Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routhledge, London (1996)"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press (2001)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"27_CR14","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"},{"issue":"2&3","key":"27_CR15","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci.\u00a072(2&3), 265\u2013288 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR16","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.\u00a0969, pp. 529\u2013539. Springer, Heidelberg (1995)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Mardare, R.: Complete proof system for weighted modal logic. In: Theoretical Computer Science (2013) (in press)","DOI":"10.1016\/j.tcs.2014.03.007"},{"key":"27_CR18","unstructured":"Larsen, K.G., Mardare, R., Xue, B.: Adequacy and strongly-complete axiomatization for timed modal logic (under review)"},{"key":"27_CR19","unstructured":"Larsen, K.G., Mardare, R., Xue, B.: Decidability and expressiveness of recursive weighted logic. In: Ershov Informatics Conference (PSI) (to appear, 2014)"},{"issue":"2","key":"27_CR20","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. Pacific Journal of Mathematics\u00a05(2), 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"issue":"1-2","key":"27_CR21","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 \u03bc-calculus. Inf. Comput.\u00a0157(1-2), 142\u2013182 (2000)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10882-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T15:44:36Z","timestamp":1746373476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10882-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108810","9783319108827"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10882-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}