{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:31Z","timestamp":1740108331072,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T00:00:00Z","timestamp":1582156800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T00:00:00Z","timestamp":1582156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61625206","61732001"],"award-info":[{"award-number":["61625206","61732001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Advanced Project FRAPPANT 787914"],"award-info":[{"award-number":["Advanced Project FRAPPANT 787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG RTG 1765 SCARE"],"award-info":[{"award-number":["DFG RTG 1765 SCARE"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["DFG FR 2715\/4"],"award-info":[{"award-number":["DFG FR 2715\/4"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61502467"],"award-info":[{"award-number":["61502467"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA2386-17-1-4022"],"award-info":[{"award-number":["FA2386-17-1-4022"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing and actuating the environment through physical devices nor data forwarding to and from the controller and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play and to submit these decisions well before they can take effect asynchronously. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm successively synthesizing a series of controllers handling increasing delays and reducing the game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore address the practically relevant cases of non-order-preserving delays and bounded message loss, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay.<\/jats:p>","DOI":"10.1007\/s00236-020-00374-7","type":"journal-article","created":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T06:15:00Z","timestamp":1582179300000},"page":"497-528","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Indecision and delays are the parents of failure\u2014taming them algorithmically by synthesizing delay-resilient control"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"first","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Yangjia","family":"Li","sequence":"additional","affiliation":[]},{"given":"Peter N.","family":"Mosaad","sequence":"additional","affiliation":[]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"key":"374_CR1","unstructured":"Balemi, S.: Communication delays in connections of input\/output discrete event processes. In: CDC 1992, pp. 3374\u20133379 (1992)"},{"key":"374_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, S., Namjoshi, K.S., Sa\u2019ar, Y.: Synthesis of asynchronous reactive programs from temporal specifications. In: CAV 2018, pp. 367\u2013385 (2018)","DOI":"10.1007\/978-3-319-96145-3_20"},{"key":"374_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games! In: CAV 2007, Lecture Notes in Computer Science, vol. 4590, pp. 121\u2013125 (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"issue":"3","key":"374_CR4","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1051\/ita:2002013","volume":"36","author":"J Bernet","year":"2002","unstructured":"Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. Theoret. Informat. Appl. 36(3), 261\u2013275 (2002)","journal-title":"Theoret. Informat. Appl."},{"key":"374_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: VMCAI 2014, Lecture Notes in Computer Science, vol. 8318, pp. 1\u201320 (2014)","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"374_CR6","doi-asserted-by":"crossref","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT 2014, EPTCS, vol. 157, pp. 100\u2013116 (2014)","DOI":"10.4204\/EPTCS.157.11"},{"key":"374_CR7","doi-asserted-by":"crossref","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J., Sankur, O.: Compositional algorithms for succinct safety games. In: SYNT 2015, pp. 98\u2013111 (2015)","DOI":"10.4204\/EPTCS.202.7"},{"key":"374_CR8","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Am. Math. Soc."},{"issue":"1","key":"374_CR9","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295\u2013311 (1969)","journal-title":"Trans. Am. Math. Soc."},{"issue":"3","key":"374_CR10","first-page":"1","volume":"3","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.: Algorithms for omega-regular games with imperfect information. Log. Methods Comput. Sci. 3(3), 1\u201323 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"374_CR11","doi-asserted-by":"crossref","unstructured":"Chen, M., Fr\u00e4nzle, M., Li, Y., Mosaad, P.N., Zhan, N.: What\u2019s to come is still unsure \u2014 synthesizing controllers resilient to delayed interaction. In: ATVA 2018, Lecture Notes in Computer Science, vol. 11138, pp. 56\u201374 (2018)","DOI":"10.1007\/978-3-030-01090-4_4"},{"key":"374_CR12","unstructured":"De Giacomo, G., Vardi, M.Y.: LTL$$_f$$ and LDL$$_f$$ synthesis under partial observability. In: IJCAI 2016, pp. 1044\u20131050 (2016)"},{"issue":"3","key":"374_CR13","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1109\/T-C.1969.222636","volume":"18","author":"S Even","year":"1969","unstructured":"Even, S., Meyer, A.R.: Sequential boolean equations. IEEE Trans. Comput. 18(3), 230\u2013240 (1969)","journal-title":"IEEE Trans. Comput."},{"key":"374_CR14","first-page":"28","volume":"266","author":"D Gale","year":"1953","unstructured":"Gale, D., Stewart, F.M.: Infinite games with perfect information. Contrib. Theory Games II Ann. Math. Stud. 266, 28\u2013245 (1953)","journal-title":"Contrib. Theory Games II Ann. Math. Stud."},{"key":"374_CR15","unstructured":"Holtmann, M.: Memory and delay in regular infinite games. Ph.D. thesis, RWTH Aachen (2011)"},{"issue":"3","key":"374_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(3:24)2012","volume":"8","author":"M Holtmann","year":"2012","unstructured":"Holtmann, M., Kaiser, L., Thomas, W.: Degrees of lookahead in regular infinite games. Log Methods Comput Sci 8(3), 1\u201315 (2012)","journal-title":"Log Methods Comput Sci"},{"key":"374_CR17","unstructured":"Hosch, F.A., Landweber, L.H.: Finite delay solutions for sequential conditions. In: ICALP 1972, pp. 45\u201360 (1972)"},{"key":"374_CR18","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: SYNT@CAV 2016, pp. 112\u2013132 (2016)","DOI":"10.4204\/EPTCS.229.10"},{"key":"374_CR19","doi-asserted-by":"crossref","unstructured":"Klein, F., Zimmermann, M.: How much lookahead is needed to win infinite games? In: ICALP 2015, Lecture Notes in Computer Science, vol. 9135, pp. 452\u2013463 (2015)","DOI":"10.1007\/978-3-662-47666-6_36"},{"key":"374_CR20","unstructured":"Klein, F., Zimmermann, M.: What are strategies in delay games? Borel determinacy for games with lookahead. In: CSL 2015, Leibniz International Proceedings in Informatics, vol. 41, pp. 519\u2013533 (2015)"},{"key":"374_CR21","doi-asserted-by":"crossref","unstructured":"Klein, U., Piterman, N., Pnueli, A.: Effective synthesis of asynchronous systems from GR(1) specifications. In: VMCAI 2012, pp. 283\u2013298 (2012)","DOI":"10.1007\/978-3-642-27940-9_19"},{"key":"374_CR22","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic. Springer, Berlin, pp. 109\u2013127 (2000)","DOI":"10.1007\/978-94-015-9586-5_6"},{"issue":"2","key":"374_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0168-0072(93)90036-D","volume":"65","author":"R McNaughton","year":"1993","unstructured":"McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149\u2013184 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"5","key":"374_CR24","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1109\/TAC.2006.872834","volume":"51","author":"S Park","year":"2006","unstructured":"Park, S., Cho, K.: Delay-robust supervisory control of discrete-event systems with bounded communication delays. IEEE Trans. Autom. Control 51(5), 911\u2013915 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"key":"374_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: ICALP 1989, Lecture Notes in Computer Science, vol. 327, pp. 652\u2013671 (1989)","DOI":"10.1007\/BFb0035790"},{"issue":"2","key":"374_CR26","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/0022-0000(84)90034-5","volume":"29","author":"JH Reif","year":"1984","unstructured":"Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274\u2013301 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"374_CR27","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: ATVA 2007, pp. 474\u2013488 (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"374_CR28","unstructured":"Somenzi, F.: Binary decision diagrams. In: Calculational System Design, volume 173 of NATO Science Series F: Computer and Systems Sciences. IOS Press, Amsterdam, pp. 303\u2013366 (1999)"},{"key":"374_CR29","doi-asserted-by":"crossref","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: STACS 95, Lecture Notes in Computer Science, vol. 900, pp. 1\u201313 (1995)","DOI":"10.1007\/3-540-59042-0_57"},{"issue":"9","key":"374_CR30","doi-asserted-by":"publisher","first-page":"1489","DOI":"10.1109\/TAC.2004.834116","volume":"49","author":"S Tripakis","year":"2004","unstructured":"Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489\u20131501 (2004)","journal-title":"IEEE Trans. Autom. Control"},{"key":"374_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: CAV 1995, pp. 267\u2013278 (1995)","DOI":"10.1007\/3-540-60045-0_56"},{"key":"374_CR32","doi-asserted-by":"crossref","unstructured":"Wulf, M.D., Doyen, L., Raskin, J.: A lattice theory for solving games of imperfect information. In: HSCC 2006, Lecture Notes in Computer Science, vol. 3927, pp. 153\u2013168 (2006)","DOI":"10.1007\/11730637_14"},{"key":"374_CR33","doi-asserted-by":"crossref","unstructured":"Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, EPTCS, vol. 256, pp. 151\u2013165 (2017)","DOI":"10.4204\/EPTCS.256.11"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00374-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00374-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00374-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T10:10:44Z","timestamp":1630059044000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00374-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,20]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["374"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00374-7","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2020,2,20]]},"assertion":[{"value":"16 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}