{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T19:36:32Z","timestamp":1769974592877,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319469812","type":"print"},{"value":"9783319469829","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46982-9_21","type":"book-chapter","created":{"date-parts":[[2016,9,19]],"date-time":"2016-09-19T11:41:08Z","timestamp":1474285268000},"page":"333-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Finite-Trace Linear Temporal Logic: Coinductive Completeness"],"prefix":"10.1007","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,20]]},"reference":[{"key":"21_CR1","first-page":"181","volume-title":"Handbook of Philosophical Logic","author":"SN Artemov","year":"2005","unstructured":"Artemov, S.N., Beklemishev, L.D.: Provability logic. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. XIII, 2nd edn, pp. 181\u2013360. Springer, Berlin (2005)","edition":"2"},{"issue":"3","key":"21_CR2","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. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"issue":"2","key":"21_CR3","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1137\/0212024","volume":"12","author":"JA Bergstra","year":"1983","unstructured":"Bergstra, J.A., Tucker, J.V.: Initial and final algebra semantics for data type specifications: two characterization theorems. SIAM J. Comput. 12(2), 366\u2013387 (1983)","journal-title":"SIAM J. Comput."},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, C., Mereu\u0163\u0103, R., Moore, B.M., \u015eerb\u0103nut\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Heidelberg (2014)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M D\u2019Amorim","year":"2005","unstructured":"D\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of omega-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364\u2013378. Springer, Heidelberg (2005)"},{"issue":"2","key":"21_CR6","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1006\/jcss.2001.1817","volume":"64","author":"V Diekert","year":"2002","unstructured":"Diekert, V., Gastin, P.: Ltl is expressively complete for mazurkiewicz traces. J. Comput. Syst. Sci. 64(2), 396\u2013418 (2002)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR8","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: ASE, pp. 412\u2013416. IEEE Computer Society (2001)"},{"key":"21_CR9","series-title":"CSLI Lecture Notes","volume-title":"Logics of Time and Computation","author":"R Goldblatt","year":"1992","unstructured":"Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes, vol. 7, 2nd edn. Center for the Study of Language and Information, Stanford (1992)","edition":"2"},{"issue":"5\u20136","key":"21_CR10","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S1570-8683(03)00008-9","volume":"1","author":"R Goldblatt","year":"2003","unstructured":"Goldblatt, R.: Mathematical modal logic: a view of its evolution. J. Appl. Log. 1(5\u20136), 309\u2013392 (2003)","journal-title":"J. Appl. Log."},{"key":"21_CR11","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Rosu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. (STTT) 6, 158\u2013173 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"10","key":"21_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-52148-8_16","volume-title":"Automatic Verification Methods for Finite State Systems","author":"C Jard","year":"1990","unstructured":"Jard, C., Jeron, T.: On-line model-checking for finite linear temporal logic specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 189\u2013196. Springer, Heidelberg (1990). doi:\n                      10.1007\/3-540-52148-8_16"},{"key":"21_CR14","unstructured":"Kamp, H.W.: Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles (1968)"},{"key":"21_CR15","first-page":"279","volume-title":"PDPTA","author":"I Lee","year":"1999","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Arabnia, H.R. (ed.) PDPTA, pp. 279\u2013287. CSREA Press, Las Vegas (1999)"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Log. J. IGPL 8(1), 55\u201385 (2000)","journal-title":"Log. J. IGPL"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Log. Progr.","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Log. Progr. LNCS, vol. 193, pp. 196\u2013218. Springer, Berlin, Heidelberg (1985)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, C., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Symposium on Logic in Computer Science (LICS 2013), pp. 358\u2013367. IEEE, June 2013","DOI":"10.1109\/LICS.2013.42"},{"key":"21_CR20","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Rosu","year":"2005","unstructured":"Rosu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12, 151\u2013197 (2005). doi:\n                      10.1007\/s10515-005-6205-y","journal-title":"Autom. Softw. Eng."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A.: Checking reachability using matching logic. In: Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2384616.2384656"},{"issue":"3","key":"21_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-30473-6_11","volume-title":"Tests and Proofs","author":"M Sulzmann","year":"2012","unstructured":"Sulzmann, M., Zechner, A.: Constructive finite trace analysis with linear temporal logic. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 132\u2013148. Springer, Heidelberg (2012)"},{"issue":"2","key":"21_CR24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1006\/inco.2001.2956","volume":"179","author":"P Thiagarajan","year":"2002","unstructured":"Thiagarajan, P., Walukiewicz, I.: An expressively complete linear time temporal logic for mazurkiewicz traces. Inf. Comput. 179(2), 230\u2013249 (2002)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46982-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:28:57Z","timestamp":1558315737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46982-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319469812","9783319469829"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46982-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"20 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}