{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:15Z","timestamp":1740122775701,"version":"3.37.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["1464\/18"],"award-info":[{"award-number":["1464\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s10703-023-00429-8","type":"journal-article","created":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T04:19:11Z","timestamp":1687493951000},"page":"405-425","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On monitoring linear temporal properties"],"prefix":"10.1007","volume":"60","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7280-6578","authenticated-orcid":false,"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,22]]},"reference":[{"issue":"3","key":"429_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117\u2013126","journal-title":"Distrib Comput"},{"key":"429_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on runtime verification\u2013introductory and advanced topics, LNCS","author":"E Bartocci","year":"2018","unstructured":"Bartocci E, Falcone Y, Francalanza A, Leucker M, Reger G (2018) An introduction to runtime verification. Lectures on runtime verification\u2013introductory and advanced topics, LNCS, vol 10457. Springer, Berlin, pp 1\u201323"},{"issue":"12","key":"429_CR3","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1016\/j.ipl.2014.06.005","volume":"114","author":"DA Basin","year":"2014","unstructured":"Basin DA, Jim\u00e9nez CC, Klaedtke F, Zalinescu E (2014) Deciding safety and liveness in TPTL. Inf. Process. Lett. 114(12):680\u2013688","journal-title":"Inf. Process. Lett."},{"key":"429_CR4","doi-asserted-by":"crossref","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly?. In: RV\u201907, LNCS, vol 4839. Springer, pp 126\u2013138","DOI":"10.1007\/978-3-540-77395-5_11"},{"issue":"4","key":"429_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):1\u201364","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"429_CR6","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer B, K\u00f6nighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: TACAS, pp 533\u2013548","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"429_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model-checking. In: CONCUR, pp 135\u2013150","DOI":"10.1007\/3-540-63141-0_10"},{"key":"429_CR8","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"429_CR9","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge"},{"key":"429_CR10","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.tcs.2014.02.052","volume":"537","author":"V Diekert","year":"2014","unstructured":"Diekert V, Leucker M (2014) Topology, monitorable properties and runtime verification. Theor Comput Sci 537:29\u201341","journal-title":"Theor Comput Sci"},{"key":"429_CR11","unstructured":"Drissi-Kaitouni O, Jard C (1988) Compiling temporal logic specifications into observers. INRIA Research Report RR-0881"},{"key":"429_CR12","doi-asserted-by":"crossref","unstructured":"Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: ICALP, pp 169\u2013181","DOI":"10.1007\/3-540-10003-2_69"},{"key":"429_CR13","doi-asserted-by":"crossref","unstructured":"Falcone Y, Fernandez J-C, Mounier L (2009) Runtime verification of safety\/progress properties. In: RV\u201909, LNCS, vol 5779. Springer, pp 40\u201359","DOI":"10.1007\/978-3-642-04694-0_4"},{"issue":"3","key":"429_CR14","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? STTT 14(3):349\u2013382","journal-title":"STTT"},{"issue":"1\u20132","key":"429_CR15","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0167-6423(96)00032-9","volume":"29","author":"J-C Fernandez","year":"1997","unstructured":"Fernandez J-C, Jard C, J\u00e9ron T, Viho C (1997) An experiment in automatic generation of test suites for protocols with verification technology. Sci Comput Program 29(1\u20132):123\u2013146","journal-title":"Sci Comput Program"},{"key":"429_CR16","series-title":"Summer school Marktoberdorf 2012-Engineering dependable software systems","first-page":"141","volume-title":"A tutorial on runtime verification","author":"Y Falcone","year":"2013","unstructured":"Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. Summer school Marktoberdorf 2012-Engineering dependable software systems. IOS Press, Amsterdam, pp 141\u2013175"},{"key":"429_CR17","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled DA, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"429_CR18","first-page":"61","volume-title":"Monitoring events that carry data, lectures on runtime verification\u2014introductory and advanced topics, LNCS","author":"K Havelund","year":"2018","unstructured":"Havelund K, Reger G, Thoma D, Z\u0103linescu E (2018) Monitoring events that carry data, lectures on runtime verification\u2014introductory and advanced topics, LNCS, vol 10457. Springer, Berlin, pp 61\u2013102"},{"key":"429_CR19","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. IN: TACAS\u201902, LNCS, vol 2280. Springer, pp 342\u2013356","DOI":"10.1007\/3-540-46002-0_24"},{"key":"429_CR20","doi-asserted-by":"crossref","unstructured":"Isberner M, Howar F, Steffen B (2014) The TTT algorithm: a redundancy-free approach to active automata learning. In: RV\u201914, LNCS, vol 8734. Springer, pp 307\u2013322","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"429_CR21","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10994-013-5419-7","volume":"96","author":"M Isberner","year":"2014","unstructured":"Isberner M, Howar F, Steffen B (2014) Learning register automata: from languages to program structures. Mach Learn 96:65\u201398","journal-title":"Mach Learn"},{"key":"429_CR22","doi-asserted-by":"crossref","unstructured":"Isberner M, Howar F, Steffen B (2015) The open-source LearnLib. In: CAV\u201915, LNCS, vol 9206. Springer, pp 487\u2013495","DOI":"10.1007\/978-3-319-21690-4_32"},{"issue":"2","key":"429_CR23","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10703-017-0277-8","volume":"52","author":"O Kupferman","year":"2018","unstructured":"Kupferman O, Vardi G (2018) On relative and probabilistic finite counterability. Formal Methods Syst Des 52(2):117\u2013146","journal-title":"Formal Methods Syst Des"},{"issue":"3","key":"429_CR24","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Formal Methods Syst Des 19(3):291\u2013314","journal-title":"Formal Methods Syst Des"},{"issue":"2","key":"429_CR25","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125\u2013143","journal-title":"IEEE Trans Softw Eng"},{"key":"429_CR26","doi-asserted-by":"crossref","unstructured":"Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. In: ISoLA\u201916, LNCS, vol 9953. Springer, pp 3\u201315","DOI":"10.1007\/978-3-319-47166-2_1"},{"key":"429_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems-specification","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems-specification. Springer, Berlin"},{"key":"429_CR28","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2011) An overview of the MOP runtime verification framework. STTT 14:249\u2013289","journal-title":"STTT"},{"key":"429_CR29","first-page":"218","volume-title":"Models, mindsets, meta","author":"D Peled","year":"2018","unstructured":"Peled D, Havelund K (2018) Refining the safety-liveness classification of temporal properties according to monitorability. Models, mindsets, meta. Springer, Cham, pp 218\u2013234"},{"key":"429_CR30","doi-asserted-by":"crossref","unstructured":"Peled DA, Vardi MY, Yannakakis M (1999) Black box checking, FORTE\/PSTV\u201999.In: IFIP conference proceedings, vol 156. Kluwer, pp 225\u2013240","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"429_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM\u201906, LNCS, vol 4085. Springer, pp 573\u2013586","DOI":"10.1007\/11813040_38"},{"key":"429_CR32","doi-asserted-by":"crossref","unstructured":"Queille J-P, Sifakis J (1981) Iterative methods for the analysis of Petri nets. In: Selected papers from the first and the second European workshop on application and theory of Petri nets, pp 161\u2013167","DOI":"10.1007\/978-3-642-68353-4_27"},{"key":"429_CR33","doi-asserted-by":"crossref","unstructured":"Safra S (1988) On the complexity of omega-automata. In: FOCS, pp 319\u2013327","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"5","key":"429_CR34","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla AP (1994) Safety, liveness and fairness in temporal logic. Formal Asp Comput 6(5):495\u2013512","journal-title":"Formal Asp Comput"},{"key":"429_CR35","doi-asserted-by":"crossref","unstructured":"Sistla AP, Clarke EM (1982) The complexity of propositional linear temporal logics. In: STOC, pp 159\u2013168","DOI":"10.1145\/800070.802189"},{"key":"429_CR36","first-page":"133","volume-title":"Formal Models and Semantics","author":"W Thomas","year":"1990","unstructured":"Thomas W (1990) Automata on infinite objects, handbook of theoretical computer science, volume B. Formal Models and Semantics. Elsevier, Amsterdam, pp 133\u2013192"},{"issue":"2","key":"429_CR37","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"MY Vardi","year":"1986","unstructured":"Vardi MY, Wolper P (1986) Automata-theoretic techniques for modal logics of programs. J Comput Syst Sci 32(2):183\u2013221","journal-title":"J Comput Syst Sci"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00429-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00429-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00429-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,10]],"date-time":"2023-10-10T10:29:52Z","timestamp":1696933792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00429-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["429"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00429-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,6]]},"assertion":[{"value":"14 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 April 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}