{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:21:42Z","timestamp":1775874102586,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T00:00:00Z","timestamp":1386201600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s00236-013-0191-5","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T22:47:38Z","timestamp":1386197258000},"page":"193-220","source":"Crossref","is-referenced-by-count":54,"title":["Synthesizing robust systems"],"prefix":"10.1007","volume":"51","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karin","family":"Greimel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Hofferek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bettina","family":"K\u00f6nighofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,12,5]]},"reference":[{"issue":"4","key":"191_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"191_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta and Malik [32], pp. 240\u2013253","DOI":"10.1007\/978-3-540-70545-1_23"},{"issue":"3","key":"191_CR3","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1109\/TSE.1983.237017","volume":"9","author":"T Anderson","year":"1983","unstructured":"Anderson, T., Knight, J.C.: A framework for software fault tolerance in real-time systems. IEEE Trans. Softw. Eng. 9(3), 355\u2013364 (1983)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"11","key":"191_CR4","doi-asserted-by":"crossref","first-page":"1015","DOI":"10.1109\/32.256850","volume":"19","author":"A Arora","year":"1993","unstructured":"Arora, A., Gouda, M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Softw. Eng. 19(11), 1015\u20131027 (1993)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"191_CR5","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1145\/963778.963782","volume":"26","author":"PC Attie","year":"2004","unstructured":"Attie, P.C., Arora, A., Emerson, A.E.: Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst. 26(1), 125\u2013185 (2004)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"191_CR6","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avizienis","year":"2004","unstructured":"Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.E.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput. 1(1), 11\u201333 (2004)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"191_CR7","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: Touili et al. (eds) [49], pp. 410\u2013424","DOI":"10.1007\/978-3-642-14295-6_36"},{"key":"191_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani and Maler [14], pp. 140\u2013156","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"191_CR9","doi-asserted-by":"crossref","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., K\u00f6nighofer, R., Roveri, M., Schuppan, V., Seeber, R.: Ratsy\u2014a new requirements analysis tool with synthesis. In: Touili et al. [49], pp. 425\u2013429","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"191_CR10","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188\u20131193. ACM (2007)","DOI":"10.1109\/DATE.2007.364456"},{"issue":"4","key":"191_CR11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"191_CR12","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gamauf, H.-J., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems with RATSY. In: Peled, D., Schewe, S. (eds.) SYNT, Volume 84 of EPTCS, pp. 47\u201353 (2012)","DOI":"10.4204\/EPTCS.84.4"},{"key":"191_CR13","doi-asserted-by":"crossref","unstructured":"Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD, pp. 85\u201392. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351139"},{"key":"191_CR14","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Maler, O. (eds): Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. In: Proceedings, Volume 5643 of Lecture Notes in Computer Science. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4"},{"key":"191_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L. (2010) Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Friedhelm Meyer auf der Heide, Spirakis, P.G. (eds) ICALP (2), Volume 6199 of Lecture Notes in Computer Science, pp. 599\u2013610. Springer, Berlin","DOI":"10.1007\/978-3-642-14162-1_50"},{"key":"191_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR, Volume 5201 of Lecture Notes in Computer Science, pp. 147\u2013161. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85361-9_14"},{"key":"191_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS, pp. 178\u2013187. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.26"},{"issue":"8","key":"191_CR18","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/2240236.2240262","volume":"55","author":"S Chaudhuri","year":"2012","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM 55(8), 107\u2013115 (2012)","journal-title":"Commun. ACM"},{"key":"191_CR19","doi-asserted-by":"crossref","unstructured":"Cheng, C.-H., Rue\u00df, H., Knoll, A., Buckl, C.: Synthesis of fault-tolerant embedded systems using games: from theory to practice. In: Jhala, R., Schmidt, D.A. (eds.) VMCAI, Volume 6538 of Lecture Notes in Computer Science, pp. 118\u2013133. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_10"},{"key":"191_CR20","unstructured":"Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians (Stockholm, 1962), pp. 23\u201335. Institut Mittag-Leffler, Djursholm (1963)"},{"issue":"2","key":"191_CR21","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1109\/9.746270","volume":"44","author":"JER Cury","year":"1999","unstructured":"Cury, J.E.R., Krogh, B.H.: Robustness of supervisors for discrete-event systems. Autom. Control IEEE Trans. 44(2), 376\u2013379 (1999)","journal-title":"Autom. Control IEEE Trans."},{"issue":"11","key":"191_CR22","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"key":"191_CR23","doi-asserted-by":"crossref","unstructured":"Doyen, L., Henzinger, T.A., Legay, A., Nickovic, D.: Robustness of sequential circuits. In: Gomes, L., Khomenko, V., Fernandes, J.M. (eds.) ACSD, pp. 77\u201384. IEEE Computer Society (2010)","DOI":"10.1109\/ACSD.2010.26"},{"key":"191_CR24","doi-asserted-by":"crossref","unstructured":"D\u2019Souza, D., Gopinathan, M.: Conflict-tolerant features. In: Gupta and Malik [32], pp. 227\u2013239","DOI":"10.1007\/978-3-540-70545-1_22"},{"issue":"5","key":"191_CR25","doi-asserted-by":"crossref","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":"191_CR26","doi-asserted-by":"crossref","unstructured":"Eisner, C.: Using symbolic model checking to verify the railway stations of hoorn-kersenboogerd and heerhugowaard. In: Pierre, L., Kropf, Th (eds.) CHARME, volume 1703 of Lecture Notes in Computer Science, pp. 97\u2013109. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48153-2_9"},{"key":"191_CR27","unstructured":"Faella, M.: Games you cannot win. In: Workshop on Games and Automata for Synthesis and Validation (2007)"},{"key":"191_CR28","doi-asserted-by":"crossref","unstructured":"Fey, G., Drechsler, R.: A basis for formal robustness checking. In: ISQED, pp. 784\u2013789. IEEE Computer Society (2008)","DOI":"10.1109\/ISQED.2008.4479838"},{"key":"191_CR29","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani and Maler [14], pp. 263\u2013277","DOI":"10.1007\/978-3-642-02658-4_22"},{"issue":"1","key":"191_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/311531.311532","volume":"31","author":"FC G\u00e4rtner","year":"1999","unstructured":"G\u00e4rtner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1\u201326 (1999)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"191_CR31","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/s10703-009-0084-y","volume":"35","author":"A Girault","year":"2009","unstructured":"Girault, A., Rutten, \u00c9.: Automating the addition of fault tolerance with discrete controller synthesis. Formal Methods Syst. Des. 35(2), 190\u2013225 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"191_CR32","doi-asserted-by":"crossref","unstructured":"Gupta, A., Malik, S. (eds): Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7\u201314, 2008. Proceedings, Volume 5123 of Lecture Notes in Computer Science. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1"},{"key":"191_CR33","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC\u201982, pp. 60\u201365. ACM Press (1982)","DOI":"10.1145\/800070.802177"},{"key":"191_CR34","unstructured":"Henzinger, T.: Two challenges in embedded systems design: predictability and robustness. Philos. Trans. R. Soc. 366, 3727\u20133736 (2008)"},{"key":"191_CR35","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117\u2013124. IEEE Computer Society (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"191_CR36","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Galler, S.J., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV, Volume 4590 of Lecture Notes in Computer Science, pp. 258\u2013262. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_29"},{"issue":"3","key":"191_CR37","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1109\/TDSC.2005.29","volume":"2","author":"SS Kulkarni","year":"2005","unstructured":"Kulkarni, S.S., Ebnenasir, A.: Complexity issues in automated synthesis of failsafe fault-tolerance. IEEE Trans. Dependable Secur. Comput. 2(3), 201\u2013215 (2005)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"191_CR38","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Render, E., Tabuada, P.: Robust discrete synthesis against unspecified disturbances. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) HSCC, pp. 211\u2013220. ACM, UK (2011)","DOI":"10.1145\/1967701.1967732"},{"key":"191_CR39","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Montanari, A., Napoli, M., Parente, M. (eds) GANDALF, Vvolume 25 of EPTCS, pp. 89\u2013102 (2010)","DOI":"10.4204\/EPTCS.25.11"},{"issue":"1","key":"191_CR40","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/375360.375365","volume":"33","author":"G Navarro","year":"2001","unstructured":"Navarro, G.: A guided tour to approximate string matching. ACM Comput. Surv. 33(1), 31\u201388 (2001)","journal-title":"ACM Comput. Surv."},{"key":"191_CR41","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of rabin and streett games. In: LICS, pp. 275\u2013284. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"191_CR42","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, A.E., Namjoshi, K.S. (eds.) VMCAI, Volume 3855 of Lecture Notes in Computer Science, pp. 364\u2013380. Springer, Berlin (2006)","DOI":"10.1007\/11609773_24"},{"key":"191_CR43","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"191_CR44","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81\u201398 (1989)","journal-title":"Proc. IEEE"},{"key":"191_CR45","doi-asserted-by":"crossref","unstructured":"Rinard, M.C.: Acceptability-oriented computing. In: Crocker, R., Steele Jr, G.L. (eds.) OOPSLA Companion, pp. 221\u2013239. ACM (2003)","DOI":"10.1145\/949344.949402"},{"key":"191_CR46","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA, Volume 4762 of Lecture Notes in Computer Science, pp. 474\u2013488. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"191_CR47","unstructured":"Shivakumar, P., Kistler, M., Keckler, S.W., Burger, D., Alvisi, L.: Modeling the effect of technology trends on the soft error rate of combinational logic. In: DSN, pp. 389\u2013398. IEEE Computer Society (2002)"},{"key":"191_CR48","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, Volume 3, Chapter 7, pp. 389\u2013455. Springer, Berlin (1997)","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"191_CR49","doi-asserted-by":"crossref","unstructured":"Touili, T., Cook, B., Jackson, P. (eds.): Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15\u201319, 2010. In: Proceedings, Volume 6174 of Lecture Notes in Computer Science. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6"},{"issue":"1 &2","key":"191_CR50","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","volume":"158","author":"U Zwick","year":"1996","unstructured":"Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1 &2), 343\u2013359 (1996)","journal-title":"Theor. Comput. Sci."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-013-0191-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-013-0191-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-013-0191-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T01:51:23Z","timestamp":1746064283000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-013-0191-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,5]]},"references-count":50,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["191"],"URL":"https:\/\/doi.org\/10.1007\/s00236-013-0191-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,5]]}}}