{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:16Z","timestamp":1740109096528,"version":"3.37.3"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T00:00:00Z","timestamp":1604275200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000761","name":"Imperial College London","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000761","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When dealing with unrealizable specifications in reactive synthesis, finding the weakest environment assumptions that ensure realizability is often considered a desirable property. However, little effort has been dedicated to defining or evaluating the notion of weakness of assumptions formally. The question of whether one assumption is weaker than another is commonly interpreted by considering the implication relationship between the two or, equivalently, their language inclusion. This interpretation fails to provide any insight into the weakness of the assumptions when implication (or language inclusion) does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it cannot distinguish the weakness of assumptions expressed as fairness properties. In this paper, we propose a refined measure of weakness based on combining entropy with Hausdorff dimension, a concept that captures the notion of size of the<jats:inline-formula><jats:alternatives><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c9<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-language satisfying a linear temporal logic formula. We focus on a special subset of linear temporal logic formulae which is of particular interest in reactive synthesis, called GR(1). We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae, and propose a refined measure to cover cases when two formulae are strictly ordered by implication but have the same entropy and Hausdorff dimension. We prove the consistency between our weakness measure and logical implication, that is, if one formula implies another, the latter is weaker than the former according to our measure. We evaluate our proposed weakness measure in two contexts. The first is in computing GR(1) assumption refinements where our weakness measure is used as a heuristic to drive the refinement search towards weaker solutions. The second is in the context of quantitative model checking where it is used to measure the size of the language of a model violating a linear temporal logic formula.<\/jats:p>","DOI":"10.1007\/s00165-020-00519-y","type":"journal-article","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T13:03:42Z","timestamp":1604322222000},"page":"27-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Weakness Measure for GR(1) Formulae"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0252-8218","authenticated-orcid":false,"given":"Davide G.","family":"Cavezza","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dalal","family":"Alrajeh","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"Gy\u00f6rgy","sequence":"additional","affiliation":[{"name":"DeepMind, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-642-39799-8_32","volume-title":"International conference on computer aided verification (CAV)","author":"Almagor S","year":"2013"},{"unstructured":"Asarin E Blockelet M Degorre A (2014) Entropy model checking. In: Workshop on Quantitative Aspects of Programming Languages (QAPL)\u2014joint with european joint conference on theory and practice of software (ETAPS)","key":"e_1_2_1_2_2_2"},{"doi-asserted-by":"crossref","unstructured":"Asarin E Blockelet M Degorre A Dima C Mu C (2014) Asymptotic behaviour in temporal logic. In: Joint meeting of the annual conference on computer science logic and the annual symposium on logic in computer science (CSL\/LICS). ACM Press pp 1\u20139","key":"e_1_2_1_2_3_2","DOI":"10.1145\/2603088.2603158"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_4_2","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_2_1_2_5_2","first-page":"26","volume-title":"International conference on formal methods in computer-aided design (FMCAD)","author":"Alur R","year":"2013"},{"key":"e_1_2_1_2_6_2","first-page":"501","volume-title":"International conference on tools and algorithms for the construction and analysis of systems (TACAS)","author":"Alur R","year":"2015"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"International conference on computer aided verification (CAV)","author":"Bloem R","year":"2010"},{"issue":"3","key":"e_1_2_1_2_8_2","first-page":"193","volume":"51","author":"Bloem R","year":"2014","journal-title":"Synthesizing robust systems. Acta Inf"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"International conference on computer aided verification (CAV)","author":"Bloem R","year":"2009"},{"doi-asserted-by":"crossref","unstructured":"Braberman V D'Ippolito N Piterman N Sykes D Uchitel S (2013) Controller synthesis: from modelling to enactment. In: International Conference on Software Engineering (ICSE) pp 1347\u20131350. IEEE","key":"e_1_2_1_2_10_2","DOI":"10.1109\/ICSE.2013.6606714"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_11_2","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_2_1_2_12_2","first-page":"95","volume-title":"International conference and tools and algorithms for the construction and analysis of systems (TACAS)","author":"Babiak T","year":"2012"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_13_2","DOI":"10.1137\/1.9781611971262"},{"doi-asserted-by":"crossref","unstructured":"Cavezza DG Alrajeh D (2016) Interpolation-based GR(1) assumptions refinement. CoRR arXiv:1611.07803","key":"e_1_2_1_2_14_2","DOI":"10.1007\/978-3-662-54577-5_16"},{"key":"e_1_2_1_2_15_2","first-page":"281","volume-title":"International conference on tools and algorithms for the construction and analysis of systems (TACAS)","author":"Cavezza DG","year":"2017"},{"doi-asserted-by":"crossref","unstructured":"Cavezza DG Alrajeh D Gy\u00f6rgy A (2018) A weakness measure for GR(1) formulae. In: International symposium on formal methods (FM) pp 110\u2013128","key":"e_1_2_1_2_16_2","DOI":"10.1007\/978-3-319-95582-7_7"},{"key":"e_1_2_1_2_17_2","first-page":"179","volume-title":"International conference on the quantitative evaluation of systems (QEST)","author":"Chatterjee K","year":"2006"},{"key":"e_1_2_1_2_18_2","first-page":"331","volume-title":"International conference on tools and algorithms for the construction and analysis of systems (TACAS)","author":"Cobleigh JM","year":"2003"},{"key":"e_1_2_1_2_19_2","first-page":"147","volume-title":"International conference on concurrency theory (CONCUR)","author":"Chatterjee K","year":"2008"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_20_2","DOI":"10.1016\/j.tcs.2009.02.029"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_21_2","DOI":"10.1007\/978-0-387-68612-7"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"International conference on verification, model checking, and abstract interpretation (VMCAI)","author":"Cimatti A","year":"2008"},{"key":"e_1_2_1_2_23_2","volume-title":"Elements of information theory","author":"Cover TM","year":"2006","edition":"2"},{"doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1999) Patterns in property specifications for finite-state verification. In: International conference on software engineering (ICSE). ACM pp 411\u2013420","key":"e_1_2_1_2_24_2","DOI":"10.1145\/302405.302672"},{"unstructured":"https:\/\/gitlab.doc.ic.ac.uk\/dgc14\/FMextRepo","key":"e_1_2_1_2_25_2"},{"doi-asserted-by":"crossref","unstructured":"D'Ippolito N Braberman V Kramer J Magee J Sykes D Uchitel S (2014) Hope for the best prepare for the worst: multi-tier control for adaptive systems. In: International conference on software engineering (ICSE) pp 688\u2013699","key":"e_1_2_1_2_26_2","DOI":"10.1145\/2568225.2568264"},{"doi-asserted-by":"crossref","unstructured":"D'Ippolito NR Braberman V Piterman N Uchitel S (2010) Synthesis of live behaviour models. In: International symposium on foundations of software engineering (FSE). ACM Press p 77","key":"e_1_2_1_2_27_2","DOI":"10.1145\/1882291.1882305"},{"doi-asserted-by":"crossref","unstructured":"D'Ippolito N Braberman V Sykes D Uchitel S (2015) Robust degradation and enhancement of robot mission behaviour in unpredictable environments. In: International workshop on control theory for software engineering (CTSE). ACM pp 26\u201333","key":"e_1_2_1_2_28_2","DOI":"10.1145\/2804337.2804342"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","first-page":"1125","DOI":"10.1145\/3180155.3180261","volume-title":"International conference on software engineering (ICSE)","author":"Degiovanni R","year":"2018"},{"doi-asserted-by":"crossref","unstructured":"Dimitrova R Ghasemi M Topcu U (2018) Maximum realizability for linear temporal logic specifications. In: International symposium on automated technology for verification and analysis (ATVA). Springer Berlin pp 458\u2013475","key":"e_1_2_1_2_30_2","DOI":"10.1007\/978-3-030-01090-4_27"},{"doi-asserted-by":"crossref","unstructured":"Duret-Lutz A Lewkowicz A Fauchille A Michaud T Renault E Xu L (2016) Spot 2.0\u2014a framework for LTL and \u03c9-automata manipulation. In: International symposium on automated technology for verification and analysis (ATVA). Springer Berlin pp 122\u2013129","key":"e_1_2_1_2_31_2","DOI":"10.1007\/978-3-319-46520-3_8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_32_2","DOI":"10.1007\/s10703-016-0259-2"},{"volume-title":"Fractal geometry: mathematical foundations and applications","year":"2004","author":"Falconer K","key":"e_1_2_1_2_33_2"},{"doi-asserted-by":"crossref","unstructured":"Giannakopoulou D Lerda F (2002) From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: International conference on formal techniques for networked and distributed sytems (FORTE) pp 308\u2013326","key":"e_1_2_1_2_34_2","DOI":"10.1007\/3-540-36135-9_20"},{"doi-asserted-by":"crossref","unstructured":"Giannakopoulou D Magee J (2003) Fluent model checking for event-based systems. In: European software engineering conference held jointly with international symposium on foundations of software engineering (ESEC\/FSE). ACM pp 257\u2013266","key":"e_1_2_1_2_35_2","DOI":"10.1145\/949952.940106"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_36_2","DOI":"10.5555\/938135"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_37_2","DOI":"10.1145\/1707801.1706319"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_38_2","DOI":"10.5555\/5509"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_39_2","DOI":"10.1007\/BF01211866"},{"doi-asserted-by":"crossref","unstructured":"Horn RA Johnson CR (2012) Matrix analysis","key":"e_1_2_1_2_40_2","DOI":"10.1017\/CBO9781139020411"},{"key":"e_1_2_1_2_41_2","first-page":"273","volume-title":"International conference on concurrency theory (CONCUR)","author":"Henzinger TA","year":"2013"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"International conference on computer aided verification (CAV)","author":"Kret\u00ednsk\u00fd J","year":"2012"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_43_2","DOI":"10.1109\/TRO.2009.2030225"},{"doi-asserted-by":"crossref","unstructured":"Konighofer R Hofferek G Bloem R (2009) Debugging formal specifications using simple counterstrategies. In: International conference on formal methods in computer-aided design (FMCAD) pp 152\u2013159","key":"e_1_2_1_2_44_2","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"e_1_2_1_2_45_2","first-page":"362","volume-title":"European software engineering conference held jointly with international symposium on foundations of software engineering (ESEC\/FSE), number 1","author":"Kuvent A","year":"2017"},{"key":"e_1_2_1_2_46_2","first-page":"88","volume-title":"International conference on current trends in theory and practice of computer science (SOFSEM)","author":"Kupferman O","year":"2012"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska M (2007) Quantitative verification: models techniques and tools. In: European software engineering conference held jointly with international symposium on foundations of software engineering (ESEC\/FSE). ACM Press p 449","key":"e_1_2_1_2_47_2","DOI":"10.1145\/1295014.1295018"},{"doi-asserted-by":"crossref","unstructured":"Li W Dworkin L Seshia SA (2011) Mining assumptions for synthesis. In: International conference on formal methods and models for codesign (MEMOCODE). ACM\/IEEE pp 43\u201350","key":"e_1_2_1_2_48_2","DOI":"10.1109\/MEMCOD.2011.5970509"},{"doi-asserted-by":"crossref","unstructured":"Lomuscio A Strulo B Walker N Wu P (2010) Assume-guarantee reasoning with local specifications. In: International conference on formal engineering methods (ICFEM) pp 204\u2013219","key":"e_1_2_1_2_49_2","DOI":"10.1007\/978-3-642-16901-4_15"},{"doi-asserted-by":"crossref","unstructured":"Lutz AD (2014) LTL translation improvements in spot 1.0. Int J Crit Comput Based Syst 5(1\/2):31","key":"e_1_2_1_2_50_2","DOI":"10.1504\/IJCCBS.2014.059594"},{"key":"e_1_2_1_2_51_2","first-page":"96","volume-title":"European software engineering conference held jointly with international symposium on foundations of software engineering (ESEC\/FSE), number 1","author":"Maoz S","year":"2015"},{"doi-asserted-by":"crossref","unstructured":"Maoz S Ringert JO Shalom R (2019) Symbolic repairs for GR(1) specifications. In: Proceedings of the international conference on software engineering (ICSE)","key":"e_1_2_1_2_52_2","DOI":"10.1109\/ICSE.2019.00106"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_53_2","DOI":"10.1051\/ita\/1994283-403611"},{"doi-asserted-by":"crossref","unstructured":"Nam W Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: International symposium on automated technology for verification and analysis (ATVA) pp 170\u2013185","key":"e_1_2_1_2_54_2","DOI":"10.1007\/11901914_15"},{"doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Annual symposium on foundations of computer science pp 46\u201357","key":"e_1_2_1_2_55_2","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_56_2","first-page":"364","volume-title":"International conference on verification, model checking, and abstract interpretation (VMCAI)","author":"Piterman N","year":"2006"},{"key":"e_1_2_1_2_57_2","first-page":"179","volume-title":"Principles of programming languages (POPL)","author":"Pnueli A","year":"1989"},{"key":"e_1_2_1_2_58_2","first-page":"668","volume-title":"International conference on logic for programming artificial intelligence and reasoning (LPAR)","author":"Renault E","year":"2013"},{"doi-asserted-by":"crossref","unstructured":"Somenzi F Bloem R (2000) Efficient Buchi automata from LTL formulae. In: International conference on computer aided verification (CAV) vol 1855 pp 1\u201317","key":"e_1_2_1_2_59_2","DOI":"10.1007\/10722167_21"},{"volume-title":"Non-negative matrices and Markov chains","year":"2006","author":"Seneta E","key":"e_1_2_1_2_60_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_61_2","DOI":"10.1109\/JPROC.2015.2471838"},{"unstructured":"Staiger L (1998) The Hausdorff measure of regular \u03c9-languages is computable. Technical Report August Martin-Luther-Universit\u00e4t","key":"e_1_2_1_2_62_2"},{"issue":"1","key":"e_1_2_1_2_63_2","first-page":"357","article-title":"On the Hausdorff measure of regular omega-languages in Cantor space","volume":"17","author":"Staiger L","year":"2015","journal-title":"Discrete Math Theor Comput Sci"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_64_2","DOI":"10.1137\/0201010"},{"unstructured":"Tabuada P Neider D (2016) Robust linear temporal logic. In: Annual conference on computer science logic (CSL) pp 10:1\u201310:21. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik","key":"e_1_2_1_2_65_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_66_2","DOI":"10.1007\/s00236-016-0280-3"},{"doi-asserted-by":"crossref","unstructured":"Vardi MY (1996) An automata-theoretic approach to linear temporal logic. Logics for concurrency pp 238\u2013266","key":"e_1_2_1_2_67_2","DOI":"10.1007\/3-540-60915-6_6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00519-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-020-00519-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00519-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00519-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,26]],"date-time":"2022-11-26T05:47:45Z","timestamp":1669441665000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00519-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1]]},"references-count":67,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["10.1007\/s00165-020-00519-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00519-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2021,1]]},"assertion":[{"value":"20 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 September 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}