{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T15:52:23Z","timestamp":1784044343731,"version":"3.55.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030223472","type":"print"},{"value":"9783030223489","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-22348-9_14","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T13:04:54Z","timestamp":1561467894000},"page":"218-234","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Refining the Safety\u2013Liveness Classification of Temporal Properties According to Monitorability"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,26]]},"reference":[{"issue":"3","key":"14_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"issue":"12","key":"14_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, D.A., Jim\u00e9nez, C.C., Klaedtke, F., Zalinescu, E.: Deciding safety and liveness in TPTL. Inf. Process. Lett. 114(12), 680\u2013688 (2014)","journal-title":"Inf. Process. Lett."},{"key":"14_CR4","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. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"issue":"4","key":"14_CR5","doi-asserted-by":"publisher","first-page":"14:1","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. ACM Trans. Softw. Eng. Method. 20(4), 14:1\u201314:64 (2011)","journal-title":"ACM Trans. Softw. Eng. Method."},{"key":"14_CR6","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"14_CR7","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.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29\u201341 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR8","unstructured":"Drissi-Kaitouni, O., Jard, C.: Compiling temporal logic specifications into observers, INRIA Research Report RR-0881 (1988)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime Verification","author":"Y Falcone","year":"2009","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40\u201359. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04694-0_4"},{"issue":"3","key":"14_CR10","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.: What can you verify and enforce at runtime? STTT 14(3), 349\u2013382 (2012)","journal-title":"STTT"},{"issue":"1\u20132","key":"14_CR11","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.: An experiment in automatic generation of test suites for protocols with verification technology. Sci. Comput. Program. 29(1\u20132), 123\u2013146 (1997)","journal-title":"Sci. Comput. Program."},{"key":"14_CR12","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification XV","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembi\u0144ski, P., \u015aredniawa, M. (eds.) PSTV 1995. IFIPAICT, pp. 3\u201318. Springer, Boston (1996). \n                      https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-75632-5_3","volume-title":"Lectures on Runtime Verification","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Reger, G., Thoma, D., Z\u0103linescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61\u2013102. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-11164-3_26","volume-title":"Runtime Verification","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307\u2013322. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11164-3_26"},{"issue":"1\u20132","key":"14_CR16","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.: Learning register automata: from languages to program structures. Mach. Learn. 96(1\u20132), 65\u201398 (2014)","journal-title":"Mach. Learn."},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-21690-4_32","volume-title":"Computer Aided Verification","author":"M Isberner","year":"2015","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487\u2013495. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_32"},{"issue":"2","key":"14_CR18","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.: On relative and probabilistic finite counterability. Formal Meth. Syst. Des. 52(2), 117\u2013146 (2018)","journal-title":"Formal Meth. Syst. Des."},{"issue":"3","key":"14_CR19","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. Formal Meth. Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Meth. Syst. Des."},{"issue":"2","key":"14_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3\u201315. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-47166-2_1"},{"key":"14_CR22","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.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992)"},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14, 249\u2013289 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR24","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-0-387-35578-8_13","volume-title":"Formal Methods for Protocol Engineering and Distributed Systems","author":"D Peled","year":"1999","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 225\u2013240. Springer, Boston, MA (1999). \n                      https:\/\/doi.org\/10.1007\/978-0-387-35578-8_13"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573\u2013586. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11813040_38"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-04081-8_2","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C Baier","year":"2009","unstructured":"Baier, C., Bertrand, N., Gr\u00f6\u00dfer, M.: The effect of tossing coins in omega-automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 15\u201329. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04081-8_2"},{"issue":"5","key":"14_CR27","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495\u2013512 (1994)","journal-title":"Formal Aspects Comput."},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: STOC 1982, pp. 159-168 (1982)","DOI":"10.1145\/800070.802189"},{"key":"14_CR29","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects, handbook of theoretical computer science. In: Formal Models and Semantics, vol. B, pp. 133\u2013192 (1990)"},{"issue":"2","key":"14_CR30","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"MY Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 183\u2013221 (1986)","journal-title":"J. Comput. Syst. Sci."}],"container-title":["Lecture Notes in Computer Science","Models, Mindsets, Meta: The What, the How, and the Why Not?"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22348-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,26]],"date-time":"2019-06-26T19:10:12Z","timestamp":1561576212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22348-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030223472","9783030223489"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22348-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"26 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}