{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:14Z","timestamp":1740122774110,"version":"3.37.3"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,9,17]],"date-time":"2021-09-17T00:00:00Z","timestamp":1631836800000},"content-version":"vor","delay-in-days":16,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100008332","name":"Technische Universit\u00e4t Graz","doi-asserted-by":"publisher","award":["LEAD"],"award-info":[{"award-number":["LEAD"]}],"id":[{"id":"10.13039\/100008332","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":[[2021,9]]},"abstract":"Abstract<\/jats:title>In reactive synthesis, one begins with a temporal specification $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and automatically synthesizes a system $$M$$<\/jats:tex-math>\n M<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> such that $$M\\models \\varphi $$<\/jats:tex-math>\n \n M<\/mml:mi>\n \u22a7<\/mml:mo>\n \u03c6<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity<\/jats:italic>. Our conjecture is that if the synthesized system M<\/jats:italic> satisfies $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>non-vacuously<\/jats:italic>, then M<\/jats:italic> is likely to be closer to the user\u2019s intent, because it satisfies $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> in a more \u201cmeaningful\u201d way. Narrowing the gap between the formal specification and the designer\u2019s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis<\/jats:italic> method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible<\/jats:italic>, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.<\/jats:p>","DOI":"10.1007\/s10703-021-00381-5","type":"journal-article","created":{"date-parts":[[2021,9,17]],"date-time":"2021-09-17T20:02:12Z","timestamp":1631908932000},"page":"473-495","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Vacuity in synthesis"],"prefix":"10.1007","volume":"57","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masoud","family":"Ebrahimi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9169-3751","authenticated-orcid":false,"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,9,17]]},"reference":[{"key":"381_CR1","doi-asserted-by":"crossref","unstructured":"Armoni R, Fix L, Flaisher A, Grumberg O, Piterman N, Tiemeyer A, Vardi MY (2003) Enhanced vacuity detection in linear temporal logic. In: CAV, LNCS, Springer, vol 2725, pp 368\u2013380","DOI":"10.1007\/978-3-540-45069-6_35"},{"issue":"2","key":"381_CR2","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in ACTL formulas. Formal Methods Syst Des 18(2):279\u2013290","journal-title":"Formal Methods Syst Des"},{"key":"381_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, K\u00f6nighofer B, K\u00f6nighofer R (2014) Synthesizing robust systems. Acta Inf 51:193\u2013220","journal-title":"Acta Inf"},{"key":"381_CR4","doi-asserted-by":"crossref","unstructured":"Bloem R, Chatterjee K, Henzinger TA, Jobstmann B (2009) Better quality in synthesis through quantitative objectives. In: CAV, LNCS, Springer, vol 5643, pp 140\u2013156","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"381_CR5","doi-asserted-by":"crossref","unstructured":"Bloem R, Chockler H, Ebrahimi M, Strichman O (2017) Synthesizing non-vacuous systems. In: Proceedings of the 18th international conference in verification, model checking, and abstract interpretation (VMCAI), Lecture notes in computer science, Springer, vol 10145, pp 55\u201372","DOI":"10.1007\/978-3-319-52234-0_4"},{"key":"381_CR6","doi-asserted-by":"crossref","unstructured":"Bustan D, Flaisher A, Grumberg O, Kupferman O, Vardi M (2005) Regular vacuity. In: CHARME, LNCS, Springer, vol 3725, pp 191\u2013206","DOI":"10.1007\/11560548_16"},{"key":"381_CR7","doi-asserted-by":"crossref","unstructured":"Chechik M, Gurfinkel A (2004) Extending extended vacuity. In: FMCAD, LNCS, vol 3312","DOI":"10.1007\/978-3-540-30494-4_22"},{"issue":"3","key":"381_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-013-0192-6","volume":"43","author":"H Chockler","year":"2013","unstructured":"Chockler H, Gurfinkel A, Strichman O (2013) Beyond vacuity: towards the strongest passing formula. Formal Methods Syst Des 43(3):1\u20138","journal-title":"Formal Methods Syst Des"},{"key":"381_CR9","unstructured":"Church A (1963) Logic, arithmetics, and automata. In: ICM, institut Mittag-Leffler, pp 23\u201335"},{"issue":"5","key":"381_CR10","first-page":"519","volume":"15","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner B, Schewe S (2012) Bounded synthesis. Int J Softw Tools Technol Transf 15(5):519\u2013539","journal-title":"Int J Softw Tools Technol Transf"},{"key":"381_CR11","doi-asserted-by":"crossref","unstructured":"Jacobs S, Bloem R, Brenguier R, K\u00f6nighofer R, P\u00e9rez GA, Raskin J, Ryzhyk L, Sankur O, Seidl M, Tentrup L, Walker A (2015) The second reactive synthesis competition. In: SYNT","DOI":"10.1007\/s10009-016-0416-3"},{"issue":"2","key":"381_CR12","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B Jobstmann","year":"2012","unstructured":"Jobstmann B, Staber S, Griesmayer A, Bloem R (2012) Finding and fixing faults. J Comput Syst Sci 78(2):35\u201349","journal-title":"J Comput Syst Sci"},{"key":"381_CR13","doi-asserted-by":"crossref","unstructured":"Khalimov A, Jacobs S, Bloem R (2013) PARTY parameterized synthesis of token rings. In: CAV, pp 928\u2013933","DOI":"10.1007\/978-3-642-39799-8_66"},{"issue":"2","key":"381_CR14","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman O, Vardi M (2003) Vacuity detection in temporal model checking. J Softw Tools Technol Transf 4(2):224\u2013233","journal-title":"J Softw Tools Technol Transf"},{"key":"381_CR15","doi-asserted-by":"crossref","unstructured":"Namjoshi KS (2004) An efficiently checkable, proof-based formulation of vacuity in model checking. In: CAV, LNCS, Springer, vol 3114, pp 57\u201369","DOI":"10.1007\/978-3-540-27813-9_5"},{"key":"381_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"381_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: POPL, Austin, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"381_CR18","doi-asserted-by":"crossref","unstructured":"Samanta R, Deshmukh JV, Chaudhuri S (2013) Robustness analysis of networked systems. In: VMCAI, pp 229\u2013247","DOI":"10.1007\/978-3-642-35873-9_15"},{"issue":"1","key":"381_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00381-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00381-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00381-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T12:11:24Z","timestamp":1638360684000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00381-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["381"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00381-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,9]]},"assertion":[{"value":"8 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 September 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}