{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:16Z","timestamp":1740122716471,"version":"3.37.3"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T00:00:00Z","timestamp":1529971200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T00:00:00Z","timestamp":1529971200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-1421575"],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-1619275"],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"name":"IOHK"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s10703-018-0321-3","type":"journal-article","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T13:42:49Z","timestamp":1530020569000},"page":"138-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Finite-trace linear temporal logic: coinductive completeness"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3102-0421","authenticated-orcid":false,"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,26]]},"reference":[{"issue":"2","key":"321_CR1","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s00450-009-0057-9","volume":"23","author":"WMP Aalst","year":"2009","unstructured":"Aalst WMP, Pesic M, Schonenberg H (2009) Declarative workflows: balancing between flexibility and support. Comput Sci Res Dev 23(2):99\u2013113","journal-title":"Comput Sci Res Dev"},{"key":"321_CR2","unstructured":"Artemov SN, Beklemishev LD (2005) Provability logic. In: Handbook of philosophical logic, volume XIII, 2 edn, pp 181\u2013360. Springer, Berlin"},{"issue":"1","key":"321_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0004-3702(99)00071-5","volume":"116","author":"F Bacchus","year":"2000","unstructured":"Bacchus F, Kabanza F (2000) Using temporal logics to express search control knowledge for planning. Artif Intell 116(1):123\u2013191","journal-title":"Artif Intell"},{"issue":"3","key":"321_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 (2010) Comparing LTL semantics for runtime verification. J Log Comput 20(3):651\u2013674","journal-title":"J Log Comput"},{"issue":"2","key":"321_CR5","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1137\/0212024","volume":"12","author":"JA Bergstra","year":"1983","unstructured":"Bergstra JA, Tucker JV (1983) Initial and final algebra semantics for data type specifications: two characterization theorems. SIAM J Comput 12(2):366\u2013387","journal-title":"SIAM J Comput"},{"key":"321_CR6","unstructured":"Bienvenu M, Fritz C, McIlraith SA (2006) Planning with qualitative temporal preferences. In: Proceedings of the 10th international conference on principles of knowledge representation and reasoning (KR\u201906), pp 134\u2013144. AAAI Press"},{"issue":"2","key":"321_CR7","doi-asserted-by":"publisher","first-page":"520","DOI":"10.2307\/2274183","volume":"49","author":"MJ Cresswell","year":"1984","unstructured":"Cresswell MJ (1984) An incomplete decidable modal logic. J Symb Log 49(2):520\u2013527","journal-title":"J Symb Log"},{"key":"321_CR8","doi-asserted-by":"crossref","unstructured":"d\u2019Amorim M, Ro\u015fu G (2005) Efficient monitoring of $$\\omega $$-languages. In: Proceedings of the 17th international conference on computer aided verification, CAV\u201905, volume 3576 of LNCS, pp 364\u2013378. Springer","DOI":"10.1007\/11513988_36"},{"key":"321_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo G, De\u00a0Masellis R, Grasso M, Maggi FM, Montali M (2014) Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq S, Soffer P, V\u00f6lzer H (eds) Proceedings of the 12th international conference on business process management, BPM\u201914, volume 8659 of LNCS, pp 1\u201317","DOI":"10.1007\/978-3-319-10172-9_1"},{"key":"321_CR10","unstructured":"De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd international joint conference on artificial intelligence, IJCAI\u201913, pp 854\u2013860. AAAI Press"},{"key":"321_CR11","unstructured":"De Giacomo G, Vardi MY (2015) Synthesis for LTL and LDL on finite traces. In: Proceedings of the 24th international joint conference on artificial intelligence, IJCAI\u201915, pp 1558\u20131564. AAAI Press"},{"key":"321_CR12","unstructured":"De Giacomo G, Vardi MY (2016) LTL$${}_{\\text{f}}$$ and LDL$${}_{\\text{ f }}$$ synthesis under partial observability. In: Proceedings of the 25th international joint conference on artificial intelligence, IJCAI\u201916, pp 1044\u20131050. AAAI Press"},{"issue":"2","key":"321_CR13","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 (2002) LTL is expressively complete for Mazurkiewicz traces. J Comput Syst Sci 64(2):396\u2013418","journal-title":"J Comput Syst Sci"},{"issue":"2","key":"321_CR14","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer MJ, Ladner RE (1979) Propositional dynamic logic of regular programs. J Comput Syst Sci 18(2):194\u2013211","journal-title":"J Comput Syst Sci"},{"key":"321_CR15","unstructured":"Gabaldon A (2004) Precondition control and the progression algorithm. In: Proceedings of the 9th international conference on principles of knowledge representation and reasoning, KR\u201904, pp 634\u2013643. AAAI Press"},{"issue":"5","key":"321_CR16","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1016\/j.artint.2008.10.012","volume":"173","author":"AE Gerevini","year":"2009","unstructured":"Gerevini AE, Haslum P, Long D, Saetti A, Dimopoulos Y (2009) Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif Intell 173(5):619\u2013668","journal-title":"Artif Intell"},{"key":"321_CR17","unstructured":"Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th international conference on automated software engineering, pp 412\u2013416. IEEE Computer Society"},{"key":"321_CR18","unstructured":"Goldblatt R (1992) Logics of time and computation. Number 7 in CSLI Lecture Notes, 2nd edn. Center for the Study of Language and Information, Stanford, CA"},{"issue":"5\u20136","key":"321_CR19","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 (2003) Mathematical modal logic: a view of its evolution. J Appl Log 1(5\u20136):309\u2013392","journal-title":"J Appl Log"},{"issue":"2","key":"321_CR20","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund K, Ro\u015fu G (2004) Efficient monitoring of safety properties. Int J Softw Tools Technol Transfer 6(2):158\u2013173","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"10","key":"321_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","journal-title":"Commun ACM"},{"key":"321_CR22","doi-asserted-by":"crossref","unstructured":"Jard C, J\u00e9ron T (1990) On-line model checking for finite linear temporal logic specifications. In: Proceedings of the international workshop of automatic verification methods for finite state systems, volume 407 of LNCS, pp 189\u2013196. Springer","DOI":"10.1007\/3-540-52148-8_16"},{"key":"321_CR23","unstructured":"Kamp HW (1968) Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles"},{"key":"321_CR24","unstructured":"Lee I, Kannan S, Kim M, Sokolsky O, Viswanathan M (1999) Runtime assurance based on formal specifications. In: Proceedings of the international conference on parallel and distributed processing techniques and applications, PDPTA\u201999, pp 279\u2013287. CSREA Press"},{"key":"321_CR25","unstructured":"Li J, Zhang L, Pu G, Vardi MY, He J (2014) LTLf satisfiability checking. In: Proceedings of the 21st European conference on artificial intelligence, ECAI\u201914, volume 263 of frontiers in artificial intelligence and applications, pp 513\u2013518"},{"issue":"1","key":"321_CR26","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 (2000) Propositional temporal logics: decidability and completeness. Log J IGPL 8(1):55\u201385","journal-title":"Log J IGPL"},{"key":"321_CR27","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. In: Logics of programs, volume 193 of LNCS, pp 196\u2013218. Springer","DOI":"10.1007\/3-540-15648-8_16"},{"key":"321_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems\u2014specification","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems\u2014specification. Springer, Berlin"},{"key":"321_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems\u2014safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems\u2014safety. Springer, Berlin"},{"key":"321_CR30","doi-asserted-by":"crossref","unstructured":"Moore B, Pe\u00f1a L, Ro\u015fu G (2018) Program verification by coinduction. In: Proceedings of the 27th European symposium on programming, ESOP\u201918, volume 10801 of LNCS, pp 589\u2013618. Springer","DOI":"10.1007\/978-3-319-89884-1_21"},{"key":"321_CR31","doi-asserted-by":"crossref","unstructured":"Pe\u0161i\u0107 M, Bo\u0161na\u010dki D, van\u00a0der Aalst WMP (2010) Enacting declarative languages using LTL: avoiding errors and improving performance. In: Model checking software\u2014proceedings of the 17th international SPIN workshop, volume 6349 of LNCS, pp 146\u2013161. Springer","DOI":"10.1007\/978-3-642-16164-3_11"},{"key":"321_CR32","doi-asserted-by":"crossref","unstructured":"Pesic M, van\u00a0der Aalst WMP (2006) A declarative approach for flexible business processes management. In: Proceedings of the 4th international conference on business process management, BPM\u201906, volume 4102 of LNCS, pp 169\u2013180. Springer","DOI":"10.1007\/11837862_18"},{"key":"321_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science, FOCS\u201977, pp 46\u201357. IEEE Computer Society","DOI":"10.1109\/SFCS.1977.32"},{"key":"321_CR34","first-page":"120","volume":"16","author":"VN Redko","year":"1964","unstructured":"Redko VN (1964) On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal 16:120\u2013126","journal-title":"Ukrainskii Matematicheskii Zhurnal"},{"key":"321_CR35","doi-asserted-by":"crossref","unstructured":"Ro\u015fu G (2016) Finite-trace linear temporal logic: coinductive completeness. In: Proceedings of the 16th international conference on runtime verification, RV\u201916, volume 10012 of LNCS, pp 333\u2013350. Springer","DOI":"10.1007\/978-3-319-46982-9_21"},{"key":"321_CR36","doi-asserted-by":"crossref","unstructured":"Ro\u015fu G, \u015etef\u0103nescu A (2012) Checking reachability using matching logic. In: Proceedings of the 27th conference on object-oriented programming, systems, languages, and applications, OOPSLA\u201912, pp 555\u2013574. ACM","DOI":"10.1145\/2384616.2384656"},{"key":"321_CR37","doi-asserted-by":"crossref","unstructured":"Ro\u015fu G, \u015etef\u0103nescu A, Ciob\u00e2c\u0103 c, Moore BM (2013) One-path reachability logic. In Proceedings of the 28th symposium on logic in computer science, LICS\u201913, pp 358\u2013367. IEEE","DOI":"10.1109\/LICS.2013.42"},{"key":"321_CR38","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 (2005) Rewriting-based techniques for runtime verification. Autom Softw Eng 12:151\u2013197","journal-title":"Autom Softw Eng"},{"key":"321_CR39","doi-asserted-by":"crossref","unstructured":"\u015etef\u0103nescu A, Ciob\u00e2c\u0103 \u015e, Mereu\u0163\u0103 R, Moore BM, \u015eerb\u0103nu\u0163\u0103 TF, Ro\u015fu G (2014) All-path reachability logic. In: Proceedings of the 25th conference on rewriting techniques and applications and 12th conference on typed lambda calculi and applications (RTA-TLCA\u201914)","DOI":"10.1007\/978-3-319-08918-8_29"},{"issue":"1","key":"321_CR40","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa A (1966) Two complete axiom systems for the algebra of regular events. J ACM 13(1):158\u2013169","journal-title":"J ACM"},{"issue":"3","key":"321_CR41","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logics. J ACM 32(3):733\u2013749","journal-title":"J ACM"},{"key":"321_CR42","doi-asserted-by":"crossref","unstructured":"Sulzmann M, Zechner A (2012) Constructive finite trace analysis with linear temporal logic. In: Proceedings of the 6th international conference on tests and proofs, TAP\u201912, volume 7305 of LNCS, pp 132\u2013148. Springer","DOI":"10.1007\/978-3-642-30473-6_11"},{"key":"321_CR43","doi-asserted-by":"crossref","unstructured":"Sun Y, Xu W, Su J (2012) Declarative choreographies for artifacts. In: Liu C, Ludwig H, Toumani F, Yu Q (eds) Proceedings of the 10th international conference on service-oriented computing, ICSOC 2012, pp 420\u2013434. Springer","DOI":"10.1007\/978-3-642-34321-6_28"},{"issue":"2","key":"321_CR44","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 (2002) An expressively complete linear time temporal logic for Mazurkiewicz traces. Inf Comput 179(2):230\u2013249","journal-title":"Inf Comput"},{"issue":"2","key":"321_CR45","first-page":"99","volume":"23","author":"WMP van der Aalst","year":"2009","unstructured":"van der Aalst WMP, Pesic M, Schonenberg H (2009) Declarative workflows: balancing between flexibility and support. Comput Sci R&D 23(2):99\u2013113","journal-title":"Comput Sci R&D"},{"key":"321_CR46","doi-asserted-by":"crossref","unstructured":"Wilke T (1999) Classifying discrete temporal properties. In: Proceedings of the 16th annual symposium on theoretical aspects of computer science, STACS\u201999, volume 1563 of LNCS, pp 32\u201346. Springer","DOI":"10.1007\/3-540-49116-3_3"},{"issue":"1","key":"321_CR47","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper P (1983) Temporal logic can be more expressive. Inf Control 56(1):72\u201399","journal-title":"Inf Control"},{"key":"321_CR48","doi-asserted-by":"crossref","unstructured":"Zhu S, Tabajara LM, Li J, Pu G, Vardi MY (2017) Symbolic LTLf synthesis. In: Proceedings of the 26th international joint conference on artificial intelligence, IJCAI\u201917, pp 1362\u20131369. AAAI Press","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0321-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0321-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0321-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T11:56:34Z","timestamp":1661514994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0321-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,26]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["321"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0321-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,6,26]]},"assertion":[{"value":"26 June 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}