{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:28:50Z","timestamp":1750318130095,"version":"3.40.3"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)\u00a0the safety-progress hierarchy of boolean properties and (2)\u00a0the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\min $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mo>min<\/mml:mo>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-decomposed into safety and liveness parts, or alternatively, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\max $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mo>max<\/mml:mo>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_17","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"349-370","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Quantitative Safety and Liveness"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Mazzocchi","sequence":"additional","affiliation":[]},{"given":"N. Ege","family":"Sara\u00e7","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"de\u00a0Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139\u2013170 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2005.07.033","DOI":"10.1016\/j.tcs.2005.07.033"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"de\u00a0Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching metrics for quantitative transition systems. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings. Lecture Notes in Computer Science, vol.\u00a03142, pp. 97\u2013109. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_11","DOI":"10.1007\/978-3-540-27836-8_11"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"de\u00a0Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings. Lecture Notes in Computer Science, vol.\u00a02719, pp. 1022\u20131037. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_79","DOI":"10.1007\/3-540-45061-0_79"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Comput. 2(3), 117\u2013126 (1987). https:\/\/doi.org\/10.1007\/BF01782772","DOI":"10.1007\/BF01782772"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science, vol. 10457, pp. 1\u201333. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010). https:\/\/doi.org\/10.1093\/logcom\/exn075","DOI":"10.1093\/logcom\/exn075"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","DOI":"10.1145\/2000799.2000800"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05643, pp. 140\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 921\u2013962. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Log. 15(4), 27:1\u201327:25 (2014). https:\/\/doi.org\/10.1145\/2629686","DOI":"10.1145\/2629686"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A.: Approximate determinization of quantitative automata. In: D\u2019Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India. LIPIcs, vol.\u00a018, pp. 362\u2013373. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.362","DOI":"10.4230\/LIPIcs.FSTTCS.2012.362"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A.: Exact and approximate determinization of discounted-sum automata. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:10)2014","DOI":"10.2168\/LMCS-10(1:10)2014"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Commun. ACM 54(9), 78\u201387 (2011). https:\/\/doi.org\/10.1145\/1995376.1995396","DOI":"10.1145\/1995376.1995396"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Markey, N., Randour, M., Larsen, K.G., Laursen, S.: Average-energy games. Acta Informatica 55(2), 91\u2013127 (2018). https:\/\/doi.org\/10.1007\/s00236-016-0274-1","DOI":"10.1007\/s00236-016-0274-1"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21\u201335 (2012). https:\/\/doi.org\/10.1016\/j.tcs.2011.08.002","DOI":"10.1016\/j.tcs.2011.08.002"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. pp. 143\u2013202. Springer Berlin Heidelberg, Berlin, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-3-642-58041-3_5","DOI":"10.1007\/978-3-642-58041-3_5"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 23:1\u201323:38 (2010). https:\/\/doi.org\/10.1145\/1805950.1805953","DOI":"10.1145\/1805950.1805953"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. ACM Trans. Comput. Log. 18(4), 31:1\u201331:44 (2017). https:\/\/doi.org\/10.1145\/3152769","DOI":"10.1145\/3152769"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"D\u2019Antoni, L., Samanta, R., Singh, R.: Qlose: Program repair with quantitative objectives. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 383\u2013401. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_21","DOI":"10.1007\/978-3-319-41540-6_21"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Fahrenberg, U., Legay, A.: Generalized quantitative analysis of metric transition systems. In: Shan, C. (ed.) Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08301, pp. 192\u2013208. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_14","DOI":"10.1007\/978-3-319-03542-0_14"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Fahrenberg, U., Legay, A.: The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci. 538, 54\u201369 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2013.07.030","DOI":"10.1016\/j.tcs.2013.07.030"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349\u2013382 (2012). https:\/\/doi.org\/10.1007\/s10009-011-0196-8","DOI":"10.1007\/s10009-011-0196-8"},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Faran, R., Kupferman, O.: Spanning the spectrum from safety to liveness. Acta Informatica 55(8), 703\u2013732 (2018). https:\/\/doi.org\/10.1007\/s00236-017-0307-4","DOI":"10.1007\/s00236-017-0307-4"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Ferr\u00e8re, T., Henzinger, T.A., Kragl, B.: Monitoring event frequencies. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. LIPIcs, vol.\u00a0152, pp. 20:1\u201320:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.20","DOI":"10.4230\/LIPIcs.CSL.2020.20"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Ferr\u00e8re, T., Henzinger, T.A., Sara\u00e7, N.E.: A theory of register monitors. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 394\u2013403. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209194","DOI":"10.1145\/3209108.3209194"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Monitorability of expressive verdicts. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13260, pp. 693\u2013712. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_37","DOI":"10.1007\/978-3-031-06773-0_37"},{"key":"17_CR28","doi-asserted-by":"publisher","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02280, pp. 342\u2013356. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24","DOI":"10.1007\/3-540-46002-0_24"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci. Res. Dev. 28(4), 331\u2013344 (2013). https:\/\/doi.org\/10.1007\/s00450-013-0251-7","DOI":"10.1007\/s00450-013-0251-7"},{"key":"17_CR30","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: Dang, T., Stolz, V. (eds.) Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, September 28-30, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13498, pp. 200\u2013220. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_11","DOI":"10.1007\/978-3-031-17196-3_11"},{"key":"17_CR31","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08052, pp. 273\u2013287. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_20","DOI":"10.1007\/978-3-642-40184-8_20"},{"key":"17_CR32","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Monitorability under assumptions. In: Deshmukh, J., Nickovic, D. (eds.) Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12399, pp. 3\u201318. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_1","DOI":"10.1007\/978-3-030-60508-7_1"},{"key":"17_CR33","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470547","DOI":"10.1109\/LICS52264.2021.9470547"},{"key":"17_CR34","doi-asserted-by":"publisher","unstructured":"Katoen, J., Song, L., Zhang, L.: Probably safe or live. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS \u201914, Vienna, Austria, July 14 - 18, 2014. pp. 55:1\u201355:10. ACM (2014). https:\/\/doi.org\/10.1145\/2603088.2603147","DOI":"10.1145\/2603088.2603147"},{"key":"17_CR35","doi-asserted-by":"publisher","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Computational analysis of run-time monitoring - fundamentals of java-mac. In: Havelund, K., Rosu, G. (eds.) Runtime Verification 2002, RV 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a070, pp. 80\u201394. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80578-4","DOI":"10.1016\/S1571-0661(04)80578-4"},{"key":"17_CR36","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001). https:\/\/doi.org\/10.1023\/A:1011254632723","DOI":"10.1023\/A:1011254632723"},{"key":"17_CR37","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Model Checking: Advances and Applications, pp. 73\u2013121. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-57685-5_3","DOI":"10.1007\/978-3-319-57685-5_3"},{"key":"17_CR38","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z.: Quantitative verification: models techniques and tools. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, Dubrovnik, Croatia, September 3-7, 2007. pp. 449\u2013458. ACM (2007). https:\/\/doi.org\/10.1145\/1287624.1287688","DOI":"10.1145\/1287624.1287688"},{"key":"17_CR39","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"17_CR40","doi-asserted-by":"publisher","unstructured":"Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9-10, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02648, pp. 74\u201388. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_5","DOI":"10.1007\/3-540-44829-2_5"},{"key":"17_CR41","doi-asserted-by":"publisher","unstructured":"Li, Y., Droste, M., Lei, L.: Model checking of linear-time properties in multi-valued systems. Inf. Sci. 377, 51\u201374 (2017). https:\/\/doi.org\/10.1016\/j.ins.2016.10.030","DOI":"10.1016\/j.ins.2016.10.030"},{"key":"17_CR42","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257\u2013289 (1984). https:\/\/doi.org\/10.1016\/0167-6423(84)90003-0","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"Peled, D., Havelund, K.: Refining the safety-liveness classification of temporal properties according to monitorability. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 11200, pp. 218\u2013234. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-22348-9_14","DOI":"10.1007\/978-3-030-22348-9_14"},{"key":"17_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04085, pp. 573\u2013586. Springer (2006). https:\/\/doi.org\/10.1007\/11813040_38","DOI":"10.1007\/11813040_38"},{"key":"17_CR45","doi-asserted-by":"publisher","unstructured":"Qian, J., Shi, F., Cai, Y., Pan, H.: Approximate safety properties in metric transition systems. IEEE Trans. Reliab. 71(1), 221\u2013234 (2022). https:\/\/doi.org\/10.1109\/TR.2021.3139616","DOI":"10.1109\/TR.2021.3139616"},{"key":"17_CR46","doi-asserted-by":"publisher","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495\u2013512 (1994). https:\/\/doi.org\/10.1007\/BF01211865","DOI":"10.1007\/BF01211865"},{"key":"17_CR47","doi-asserted-by":"publisher","unstructured":"Thrane, C.R., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Algebraic Methods Program. 79(7), 689\u2013703 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.07.010","DOI":"10.1016\/j.jlap.2010.07.010"},{"key":"17_CR48","doi-asserted-by":"publisher","unstructured":"Weiner, S., Hasson, M., Kupferman, O., Pery, E., Shevach, Z.: Weighted safety. In: Hung, D.V., Ogawa, M. (eds.) Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08172, pp. 133\u2013147. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_11","DOI":"10.1007\/978-3-319-02444-8_11"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30829-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:59:28Z","timestamp":1682020768000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}