{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:22:09Z","timestamp":1743013329791,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319150741"},{"type":"electronic","value":"9783319150758"}],"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-319-15075-8_9","type":"book-chapter","created":{"date-parts":[[2015,1,6]],"date-time":"2015-01-06T10:05:27Z","timestamp":1420538727000},"page":"130-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Dynamic Logic for Every Season"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Madeira","sequence":"first","affiliation":[]},{"given":"Renato","family":"Neves","sequence":"additional","affiliation":[]},{"given":"Manuel A.","family":"Martins","sequence":"additional","affiliation":[]},{"given":"Lu\u00eds S.","family":"Barbosa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,1,7]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of java card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6\u201324. Springer, Heidelberg (2001)"},{"issue":"1\u20132","key":"9_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.tcs.2007.02.055","volume":"380","author":"M Droste","year":"2007","unstructured":"Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1\u20132), 69\u201386 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24771-5_11","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"H Furusawa","year":"2004","unstructured":"Furusawa, H.: The categories of kleene algebras, action algebras and action lattices are related by adjunctions. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003\/Kleene-Algebra Ws 2003. LNCS, vol. 3051, pp. 124\u2013136. Springer, Heidelberg (2004)"},{"key":"9_CR4","first-page":"323","volume":"13","author":"SF Goble","year":"1970","unstructured":"Goble, S.F.: Grades of modality. Logique et Analyse 13, 323\u2013334 (1970)","journal-title":"Logique et Analyse"},{"key":"9_CR5","unstructured":"Gottwald, S.: A Treatise on Many-Valued Logics. Studies in Logic and Computation, vol. 9. Research Studies Press (2001)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"9_CR7","unstructured":"Kozen, D.: On action algebras. manuscript in: Logic and Flow of Information, Amsterdam (1991)"},{"issue":"2","key":"9_CR8","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"9_CR9","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"issue":"5","key":"9_CR10","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1093\/jigpal\/jzu010","volume":"22","author":"B Lopes","year":"2014","unstructured":"Lopes, B., Benevides, M.R.F., Haeusler, E.H.: Propositional dynamic logic for petri nets. Logic Journal of the IGPL 22(5), 721\u2013736 (2014)","journal-title":"Logic Journal of the IGPL"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-73595-3_27","volume-title":"Automated Deduction \u2013 CADE-21","author":"O M\u00fcrk","year":"2007","unstructured":"M\u00fcrk, O., Larsson, D., H\u00e4hnle, R.: KeY-C: a tool for verification of c programs. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 385\u2013390. Springer, Heidelberg (2007)"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0004-3702(86)90031-7","volume":"28","author":"NJ Nilsson","year":"1986","unstructured":"Nilsson, N.J.: Probabilistic logic. Artif. Intell. 28(1), 71\u201387 (1986)","journal-title":"Artif. Intell."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Logical Methods in Computer Science 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:17)2012"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0018436","volume-title":"Logics in AI","author":"V Pratt","year":"1991","unstructured":"Pratt, V.: Action logic and pure induction. In: van Eijck, J. (ed.) Logics in AI. LNCS, vol. 478, pp. 97\u2013120. Springer, Heidelberg (1991)"},{"key":"9_CR16","unstructured":"van der Hoek, W.: On the semantics of graded modalities. Journal of Applied Non-Classical Logics 2(1) (1992)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15075-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T20:01:24Z","timestamp":1676923284000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15075-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319150741","9783319150758"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15075-8_9","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":"7 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}