{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:38Z","timestamp":1762459298193,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_54","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"581-595","source":"Crossref","is-referenced-by-count":14,"title":["An LTL Proof System for Runtime Verification"],"prefix":"10.1007","author":[{"given":"Clare","family":"Cini","sequence":"first","affiliation":[]},{"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"54_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-32759-9_10","volume-title":"FM 2012","author":"A. Bauer","year":"2012","unstructured":"Bauer, A., Falcone, Y.: Decentralised LTL Monitoring. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 85\u2013100. Springer, Heidelberg (2012)"},{"issue":"2","key":"54_CR2","first-page":"216","volume":"76","author":"K. Brunnler","year":"2008","unstructured":"Brunnler, K., Lange, M.: Cut-free sequent systems for temporal logic. JLAP\u00a076(2), 216\u2013225 (2008)","journal-title":"JLAP"},{"key":"54_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A. Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol.\u00a04839, pp. 126\u2013138. Springer, Heidelberg (2007)"},{"issue":"3","key":"54_CR4","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A. Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Logic and Comput.\u00a020(3), 651\u2013674 (2010)","journal-title":"Logic and Comput."},{"issue":"4","key":"54_CR5","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A. Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM\u00a020(4), 14 (2011)","journal-title":"TOSEM"},{"key":"54_CR6","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J. Bradfield","year":"1992","unstructured":"Bradfield, J., Stirling, C.: Local model-checking for infinite state spaces. TCS\u00a096, 157\u2013174 (1992)","journal-title":"TCS"},{"key":"54_CR7","unstructured":"Buss, S.R. (ed.): Handbook of Proof Theory. Elsevier (1998)"},{"key":"54_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"issue":"2","key":"54_CR9","first-page":"181","volume":"55","author":"M. Geilen","year":"2001","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. ENTCS\u00a055(2), 181\u2013199 (2001)","journal-title":"ENTCS"},{"key":"54_CR10","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/567446.567462","volume-title":"POPL","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL, pp. 163\u2013173. ACM, New York (1980)"},{"key":"54_CR11","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: ASE, pp. 135\u2013143. IEEE, Wash., DC (2001)","DOI":"10.1109\/ASE.2001.989799"},{"issue":"12","key":"54_CR12","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1016\/j.ic.2010.09.008","volume":"209","author":"K. Kojima","year":"2011","unstructured":"Kojima, K., Igarashi, A.: Constructive linear-time temporal logic: Proof systems and kripke semantics. Inf. Comput.\u00a0209(12), 1491\u20131503 (2011)","journal-title":"Inf. Comput."},{"issue":"3","key":"54_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des.\u00a019(3), 291\u2013314 (2001)","journal-title":"Form. Methods Syst. Des."},{"issue":"5","key":"54_CR14","first-page":"293","volume":"78","author":"M. Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of Runtime Verification. JLAP\u00a078(5), 293\u2013303 (2009)","journal-title":"JLAP"},{"issue":"1","key":"54_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the Temporal Picture. Theoretical Computer Science\u00a083(1), 97\u2013130 (1991)","journal-title":"Theoretical Computer Science"},{"key":"54_CR16","first-page":"46","volume-title":"SFCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: SFCS, pp. 46\u201357. IEEE, Wash., DC (1977)"},{"issue":"2","key":"54_CR17","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G. Ro\u015fu","year":"2005","unstructured":"Ro\u015fu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Automated Software Engg.\u00a012(2), 151\u2013197 (2005)","journal-title":"Automated Software Engg."},{"key":"54_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-40965-6_17","volume-title":"Advances in Computing Science \u2013 ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation","author":"K. Sen","year":"2003","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Generating optimal linear temporal logic monitors by coinduction. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol.\u00a02896, pp. 260\u2013275. Springer, Heidelberg (2003)"},{"key":"54_CR19","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. TCS\u00a089, 161\u2013177 (1991)","journal-title":"TCS"},{"key":"54_CR20","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (2000)","DOI":"10.1017\/CBO9781139168717"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:25:40Z","timestamp":1747855540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}