{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T18:40:08Z","timestamp":1751740808309,"version":"3.41.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319955810"},{"type":"electronic","value":"9783319955827"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-95582-7_7","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T14:31:17Z","timestamp":1531319477000},"page":"110-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Weakness Measure for GR(1) Formulae"],"prefix":"10.1007","author":[{"given":"Davide Giacomo","family":"Cavezza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dalal","family":"Alrajeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"Gy\u00f6rgy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"7_CR1","unstructured":"https:\/\/gitlab.doc.ic.ac.uk\/dgc14\/WeakestAssumptions"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1145\/2914770.2837628","volume":"51","author":"A Albarghouthi","year":"2016","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. ACM SIGPLAN Notices 51(1), 789\u2013801 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-642-39799-8_32","volume-title":"Computer Aided Verification","author":"S Almagor","year":"2013","unstructured":"Almagor, S., Avni, G., Kupferman, O.: Automatic generation of quality specifications. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 479\u2013494. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_32"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Moarref, S., Topcu, U.: Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in Computer-Aided Design, pp. 26\u201333 (2013)","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-662-46681-0_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2015","unstructured":"Alur, R., Moarref, S., Topcu, U.: Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 501\u2013516. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_49"},{"key":"7_CR6","unstructured":"Asarin, E., Blockelet, M., Degorre, A.: Entropy model checking. In: 12th Workshop on Quantitative Aspects of Programming Languages - Joint with European Joint Conference On Theory and Practice of Software (2014)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Asarin, E., Blockelet, M., Degorre, A., Dima, C., Mu, C.: Asymptotic behaviour in temporal logic. In: Joint Meeting CSL\/LICS, pp. 1\u20139. ACM Press (2014)","DOI":"10.1145\/2603088.2603158"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-015-0348-9","volume":"28","author":"J Barnat","year":"2016","unstructured":"Barnat, J., Bauch, P., Bene\u0161, N., Brim, L., Beran, J., Kratochv\u00edla, T.: Analysing sanity of requirements for avionics systems. Form. Asp. Comput. 28(1), 45\u201363 (2016)","journal-title":"Form. Asp. Comput."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Berman, A., Plemmons, R.: Nonnegative Matrices in the Mathematical Sciences. Society for Industrial and Applied Mathematics (1994)","DOI":"10.1137\/1.9781611971262"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14"},{"issue":"4","key":"7_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electron. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Braberman, V., D\u2019Ippolito, N., Piterman, N., Sykes, D., Uchitel, S.: Controller synthesis: from modelling to enactment. In: International Conference on Software Engineering, pp. 1347\u20131350. IEEE (2013)","DOI":"10.1109\/ICSE.2013.6606714"},{"key":"7_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, New York (2008)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-662-54577-5_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DG Cavezza","year":"2017","unstructured":"Cavezza, D.G., Alrajeh, D.: Interpolation-based GR(1) assumptions refinement. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 281\u2013297. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_16"},{"key":"7_CR16","unstructured":"Cavezza, D.G., Alrajeh, D., Gy\u00f6rgy, A.: A weakness measure for GR(1) formulae. CoRR abs\/1805.03151 (2018). http:\/\/arxiv.org\/abs\/1805.03151"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: International Conference on the Quantitative Evaluation of Systems, pp. 179\u2013188 (2006)","DOI":"10.1109\/QEST.2006.11"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-85361-9_14","volume-title":"CONCUR 2008 - Concurrency Theory","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 147\u2013161. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_14"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Cimatti","year":"2008","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52\u201367. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_9"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Sykes, D., Uchitel, S.: Robust degradation and enhancement of robot mission behaviour in unpredictable environments. In: Proceedings of the 1st International Workshop on Control Theory for Software Engineering, pp. 26\u201333 (2015)","DOI":"10.1145\/2804337.2804342"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$\u03c9-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata. Formal Methods Syst. Des. 49(3), 219\u2013271 (2016)","journal-title":"Formal Methods Syst. Des."},{"issue":"5","key":"7_CR24","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"7_CR25","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/1707801.1706319","volume":"45","author":"T Henzinger","year":"2010","unstructured":"Henzinger, T.: From Boolean to quantitative notions of correctness. ACM SIGPLAN Notices 45(1), 157 (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-40184-8_20","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 273\u2013287. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_20"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Konighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: Formal Methods in Computer-Aided Design, pp. 152\u2013159 (2009)","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27660-6_8","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"O Kupferman","year":"2012","unstructured":"Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88\u201398. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27660-6_8"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: Joint Meeting on Foundations of Software Engineering - ESEC\/FSE 2015, p. 449. ACM Press (2007)","DOI":"10.1145\/1295014.1295018"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: International Conference on Formal Methods and Models for Codesign, pp. 43\u201350 (2011)","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-16901-4_15","volume-title":"Formal Methods and Software Engineering","author":"A Lomuscio","year":"2010","unstructured":"Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Assume-guarantee reasoning with local specifications. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 204\u2013219. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16901-4_15"},{"issue":"1\/2","key":"7_CR32","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1504\/IJCCBS.2014.059594","volume":"5","author":"AD Lutz","year":"2014","unstructured":"Lutz, A.D.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1\/2), 31 (2014)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O.: GR(1) synthesis for LTL specification patterns. In: Joint Meeting on Foundations of Software Engineering - ESEC\/FSE 2015, pp. 96\u2013106. ACM Press (2015)","DOI":"10.1145\/2786805.2786824"},{"issue":"3\u20134","key":"7_CR34","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1051\/ita\/1994283-403611","volume":"28","author":"W Merzenich","year":"1994","unstructured":"Merzenich, W., Staiger, L.: Fractals, dimension, and formal languages. Informatique th\u00e9orique et applications 28(3\u20134), 361\u2013386 (1994)","journal-title":"Informatique th\u00e9orique et applications"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11901914_15","volume-title":"Automated Technology for Verification and Analysis","author":"W Nam","year":"2006","unstructured":"Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 170\u2013185. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901914_15"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-45221-5_44","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Etienne Renault","year":"2013","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized B\u00fcchi automata. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), pp. 668\u2013682 (2013)"},{"issue":"11","key":"7_CR39","doi-asserted-by":"publisher","first-page":"2036","DOI":"10.1109\/JPROC.2015.2471838","volume":"103","author":"SA Seshia","year":"2015","unstructured":"Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. IEEE 103(11), 2036\u20132051 (2015)","journal-title":"IEEE"},{"key":"7_CR40","unstructured":"Staiger, L.: The hausdorff measure of regular $$\\omega $$\u03c9-languages is computable. Martin-Luther-Universit\u00e4t, Technical report, August 1998"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Staiger, L.: On the Hausdorff measure of regular omega-languages in Cantor space. Technical report 1, Martin-Luther-Universit\u00e4t Halle-Wittenberg (2015)","DOI":"10.46298\/dmtcs.2112"},{"key":"7_CR42","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proceedings of the IEEE International Conference on Information Reuse and Integration, pp. 493\u2013498 (2004)"},{"key":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T18:22:08Z","timestamp":1751739728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}