{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:29Z","timestamp":1740108329846,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T00:00:00Z","timestamp":1572480000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T00:00:00Z","timestamp":1572480000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["ZI 1516\/1-1","GSC 209"],"award-info":[{"award-number":["ZI 1516\/1-1","GSC 209"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n<jats:p>Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications. In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions, optimally resilient strategies are positional and can be computed in quasipolynomial time.<\/jats:p>","DOI":"10.1007\/s00236-019-00345-7","type":"journal-article","created":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T13:04:21Z","timestamp":1572527061000},"page":"195-221","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Synthesizing optimally resilient controllers"],"prefix":"10.1007","volume":"57","author":[{"given":"Daniel","family":"Neider","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8143-246X","authenticated-orcid":false,"given":"Alexander","family":"Weinert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8038-2453","authenticated-orcid":false,"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,31]]},"reference":[{"issue":"1","key":"345_CR1","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/963778.963782","volume":"26","author":"PC Attie","year":"2004","unstructured":"Attie, P.C., Arora, A., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst. 26(1), 125\u2013185 (2004)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"345_CR2","first-page":"261","volume":"36","author":"J Bernet","year":"2002","unstructured":"Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. ITA 36(3), 261\u2013275 (2002)","journal-title":"ITA"},{"issue":"3\u20134","key":"345_CR3","first-page":"193","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems. Acta Inf. 51(3\u20134), 193\u2013220 (2014)","journal-title":"Synthesizing robust systems. Acta Inf."},{"key":"345_CR4","first-page":"140","volume-title":"Computer Aided Verification, Volume 5643 of LNCS","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.) Computer Aided Verification, Volume 5643 of LNCS, pp. 140\u2013156. Springer, Berlin (2009)"},{"key":"345_CR5","doi-asserted-by":"publisher","first-page":"34","DOI":"10.4204\/EPTCS.157.7","volume":"157","author":"Roderick Bloem","year":"2014","unstructured":"Bloem, R., Ehlers, R., Jacobs, S., K\u00f6nighofer, R.: How to handle assumptions in synthesis. In: Chatterjee, K., Ehlers, R., Jha, D. (eds.) SYNT, Volume 157 of EPTCS, pp. 34\u201350 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"3","key":"345_CR6","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":"345_CR7","unstructured":"Brihaye, T., Geeraerts, G., Haddad, A., Monmege, B., P\u00e9rez, G.A., Renault, G.: Quantitative games under failures. In: FSTTCS, Volume 45 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, pp. 293\u2013306 (2015)"},{"key":"345_CR8","first-page":"252","volume-title":"STOC","author":"CS Calude","year":"2017","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Hatami, H., McKenzie, P., King, V. (eds.) STOC, pp. 252\u2013263. ACM, New york (2017)"},{"key":"345_CR9","unstructured":"Chatterjee, K.: Linear time algorithm for weak parity games. arXiv \n(\n\n2008)"},{"key":"345_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.tcs.2012.07.038","volume":"458","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49\u201360 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"345_CR11","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/1614431.1614432","volume":"11","author":"K Chatterjee","year":"2009","unstructured":"Chatterjee, K., Henzinger, T.A., Horn, F.: Finitary winning in $$\\omega $$-regular games. ACM Trans. Comput. Log. 11(1), 257\u2013271 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"345_CR12","doi-asserted-by":"crossref","unstructured":"Dallal, E., Neider, D., Tabuada, P.: Synthesis of safety controllers robust to unmodeled intermittent disturbances. In: CDC, pp. 7425\u20137430. IEEE (2016)","DOI":"10.1109\/CDC.2016.7799416"},{"issue":"5","key":"345_CR13","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-008-0083-0","volume":"10","author":"A Ebnenasir","year":"2008","unstructured":"Ebnenasir, A., Kulkarni, S.S., Arora, A.: FTSyn: a framework for automatic synthesis of fault-tolerance. STTT 10(5), 455\u2013471 (2008)","journal-title":"STTT"},{"key":"345_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/2562059.2562128","volume-title":"HSCC","author":"R Ehlers","year":"2014","unstructured":"Ehlers, R., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: Fr\u00e4nzle, M., Lygeros, J. (eds.) HSCC, pp. 203\u2013212. ACM, New york (2014)"},{"key":"345_CR15","first-page":"112","volume-title":"SPIN","author":"J Fearnley","year":"2017","unstructured":"Fearnley, J., Jain, S., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: Erdogmus, H., Havelund, K. (eds.) SPIN, pp. 112\u2013121. ACM, New York (2017)"},{"issue":"2","key":"345_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-10(2:14)2014","volume":"10","author":"N Fijalkow","year":"2014","unstructured":"Fijalkow, N., Zimmermann, M.: Parity and Streett games with costs. Log. Methods Comput. Sci. 10(2), 1\u201329 (2014)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"345_CR17","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-009-0084-y","volume":"35","author":"A Girault","year":"2009","unstructured":"Girault, A., Rutten, E.: Automating the addition of fault tolerance with discrete controller synthesis. Form. Methods Syst. Des. 35(2), 190\u2013225 (2009)","journal-title":"Form. Methods Syst. Des."},{"volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research, Volume 2500 of LNCS","year":"2002","key":"345_CR18","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, Volume 2500 of LNCS. Springer, Berlin (2002)"},{"issue":"7","key":"345_CR19","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1109\/TSE.2015.2510001","volume":"42","author":"CH Huang","year":"2016","unstructured":"Huang, C.H., Peled, D.A., Schewe, S., Wang, F.: A game-theoretic foundation for the maximum software resilience against dense errors. IEEE Trans. Softw. Eng. 42(7), 605\u2013622 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"345_CR20","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Lazic, R.: Succinct progress measures for solving parity games. In: LICS, pp. 1\u20139. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005092"},{"key":"345_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22807-0","volume-title":"Logic and Games on Automatic Structures: Playing with Quantifiers and Decompositions, Volume 6810 of LNCS","author":"L Kaiser","year":"2011","unstructured":"Kaiser, L.: Logic and Games on Automatic Structures: Playing with Quantifiers and Decompositions, Volume 6810 of LNCS. Springer, Berlin (2011)"},{"key":"345_CR22","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1145\/3209108.3209115","volume-title":"LICS","author":"K Lehtinen","year":"2018","unstructured":"Lehtinen, K.: A modal $$\\mu $$ perspective on solving parity games in quasi-polynomial time. In: Dawar, A., Gr\u00e4del, E. (eds.) LICS, pp. 639\u2013648. ACM, New York (2018)"},{"issue":"3","key":"345_CR23","doi-asserted-by":"publisher","first-page":"48:1","DOI":"10.1145\/2539036.2539044","volume":"13","author":"R Majumdar","year":"2013","unstructured":"Majumdar, R., Render, E., Tabuada, P.: A theory of robust omega-regular software synthesis. ACM Trans. Embed. Comput. Syst. 13(3), 48:1\u201348:27 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"345_CR24","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"DA Martin","year":"1975","unstructured":"Martin, D.A.: Borel determinacy. Ann. Math. 102, 363\u2013371 (1975)","journal-title":"Ann. Math."},{"key":"345_CR25","doi-asserted-by":"crossref","unstructured":"Rungger, M., Zamani, M.: SCOTS: a tool for the synthesis of symbolic controllers. In: HSCC, pp. 99\u2013104. ACM, New york (2016)","DOI":"10.1145\/2883817.2883834"},{"issue":"12","key":"345_CR26","doi-asserted-by":"publisher","first-page":"3151","DOI":"10.1109\/TAC.2014.2351632","volume":"59","author":"P Tabuada","year":"2014","unstructured":"Tabuada, P., Caliskan, S.Y., Rungger, M., Majumdar, R.: Towards robustness for cyber-physical systems. IEEE Trans. Autom. Control 59(12), 3151\u20133163 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"345_CR27","unstructured":"Tabuada, P., Neider, D.: Robust linear temporal logic. In: Talbot, J.-M., Regnier, L. (eds.) CSL, Volume\u00a062 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, pp. 10:1\u201310:21. (2016)"},{"key":"345_CR28","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/2185632.2185648","volume-title":"HSCC","author":"U Topcu","year":"2012","unstructured":"Topcu, U., Ozay, N., Liu, J., Murray, R.M.: On synthesizing robust discrete controllers under modeling uncertainty. In: Dang, T., Mitchell, I.M. (eds.) HSCC, pp. 85\u201394. ACM, New York (2012)"},{"key":"345_CR29","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-32254-2_16","volume-title":"Mechanizing Mathematical Reasoning, Essays in Honor of J\u00f6rg H. Siekmann on the Occasion of His 60th Birthday, Volume 2605 of LNCS","author":"J van Benthem","year":"2005","unstructured":"van Benthem, J.: An essay on sabotage and obstruction. Mechanizing Mathematical Reasoning, Essays in Honor of J\u00f6rg H. Siekmann on the Occasion of His 60th Birthday, Volume 2605 of LNCS, pp. 268\u2013276. Springer, Berlin (2005)"},{"key":"345_CR30","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: TACAS, Volume 10805 of LNCS, pp. 291\u2013308. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-89960-2_16"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00345-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00345-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00345-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:18:30Z","timestamp":1604017110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00345-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,31]]},"references-count":30,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["345"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00345-7","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2019,10,31]]},"assertion":[{"value":"11 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 October 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}