{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T07:18:37Z","timestamp":1775027917915,"version":"3.50.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2016,10,7]],"date-time":"2016-10-07T00:00:00Z","timestamp":1475798400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s00236-016-0280-3","type":"journal-article","created":{"date-parts":[[2016,10,7]],"date-time":"2016-10-07T07:27:30Z","timestamp":1475825250000},"page":"655-692","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Safraless LTL synthesis considering maximal realizability"],"prefix":"10.1007","volume":"54","author":[{"given":"Takashi","family":"Tomita","sequence":"first","affiliation":[]},{"given":"Atsushi","family":"Ueno","sequence":"additional","affiliation":[]},{"given":"Masaya","family":"Shimakawa","sequence":"additional","affiliation":[]},{"given":"Shigeki","family":"Hagihara","sequence":"additional","affiliation":[]},{"given":"Naoki","family":"Yonezaki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,7]]},"reference":[{"key":"280_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, Dezani-Ciancaglini, G.M., Della\u00a0Rocca, S. (eds.) Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 372, pp. 1\u201317. Springer, Berlin (1989). doi:\n                        10.1007\/BFb0035748","DOI":"10.1007\/BFb0035748"},{"key":"280_CR2","doi-asserted-by":"publisher","unstructured":"Aoshima, T., Yonezaki, N.: Verification of reactive system specifications with outer event conditional formula. In: Proceedings of International Symposium on Principles of Software Evolution, 2000, pp.\u00a0189\u2013193. IEEE (2000). doi:\n                        10.1109\/ISPSE.2000.913238","DOI":"10.1109\/ISPSE.2000.913238"},{"key":"280_CR3","doi-asserted-by":"publisher","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, K\u00f6nig, C.B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 7214, pp. 95\u2013109. Springer, Berlin (2012). doi:\n                        10.1007\/978-3-642-28756-5_8","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"280_CR4","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 7795, pp. 32\u201346. Springer, Berlin (2013). doi:\n                        10.1007\/978-3-642-36742-7_3","DOI":"10.1007\/978-3-642-36742-7_3"},{"issue":"3\u20134","key":"280_CR5","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, T.A., Hofferek, G., Jobstmann, B., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems. Acta Inform. 51(3\u20134), 193\u2013220 (2014). doi:\n                        10.1007\/s00236-013-0191-5","journal-title":"Acta Inform."},{"key":"280_CR6","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 5643, pp. 140\u2013156. Springer, Berlin (2009). doi:\n                        10.1007\/978-3-642-02658-4_14","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"280_CR7","doi-asserted-by":"publisher","unstructured":"Bloem, R., Ehlers, R., Jacobs, S., K\u00f6nighofer, R.: How to handle assumptions in synthesis. In: Chatterjee, K., Ehlers, R., Jha, S. (eds.) Proceedings 3rd Workshop on Synthesis, Electronic Proceedings in Theoretical Computer Science, vol. 157, pp. 34\u201350. Open Publishing Association (2014). doi:\n                        10.4204\/EPTCS.157.7","DOI":"10.4204\/EPTCS.157.7"},{"key":"280_CR8","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e9re, V., Filiot, E., Jin, N., Raskin, J.F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 7358, pp. 652\u2013657. Springer, Berlin (2012). doi:\n                        10.1007\/978-3-642-31424-7_45","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"280_CR9","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e9re, V., Filiot, E., Raskin, J.F.: Synthesis from LTL specifications with mean-payoff objectives. In: Piterman, N., Smolka, S. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 7795, pp. 169\u2013184. Springer, Berlin (2013). doi:\n                        10.1007\/978-3-642-36742-7_12","DOI":"10.1007\/978-3-642-36742-7_12"},{"key":"280_CR10","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e8re, V., Raskin, J.F.: Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes. In: Chatterjee, K., Ehlers, R., Jha, S. (eds.) Proceedings 3rd Workshop on Synthesis, Electronic Proceedings in Theoretical Computer Science, vol. 157, pp. 51\u201367. Open Publishing Association (2014). doi:\n                        10.4204\/EPTCS.157.8","DOI":"10.4204\/EPTCS.157.8"},{"key":"280_CR11","doi-asserted-by":"publisher","unstructured":"Boker, U., Kupferman, O., Steinitz, A.: Parityizing Rabin and Streett. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a08, pp. 412\u2013423. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl (2010). doi:\n                        10.4230\/LIPIcs.FSTTCS.2010.412\n                        \n                    . \n                        http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2010\/2882","DOI":"10.4230\/LIPIcs.FSTTCS.2010.412"},{"issue":"2","key":"280_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-010-0105-x","volume":"38","author":"L Brim","year":"2011","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.: Faster algorithms for mean-payoff games. Form. Methods Syst. Des. 38(2), 97\u2013118 (2011). doi:\n                        10.1007\/s10703-010-0105-x","journal-title":"Form. Methods Syst. Des."},{"key":"280_CR13","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T., Jurdzinski, M.: Mean-payoff parity games. In: Proceedings of 20th Annual IEEE Symposium on Logic in Computer Science, 2005. LICS 2005, pp. 178\u2013187 (2005). doi:\n                        10.1109\/LICS.2005.26","DOI":"10.1109\/LICS.2005.26"},{"key":"280_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008\u2014Concurrency Theory, Lecture Notes in Computer Science, vol. 5201, pp. 147\u2013161. Springer, Berlin (2008). doi:\n                        10.1007\/978-3-540-85361-9_14","DOI":"10.1007\/978-3-540-85361-9_14"},{"issue":"3\u20134","key":"280_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s00236-013-0182-6","volume":"51","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Randour, M., Raskin, J.F.: Strategy synthesis for multi-dimensional quantitative objectives. Acta Inform. 51(3\u20134), 129\u2013163 (2014). doi:\n                        10.1007\/s00236-013-0182-6","journal-title":"Acta Inform."},{"key":"280_CR16","doi-asserted-by":"publisher","unstructured":"Damm, W., Finkbeiner, B.: Automatic compositional synthesis of distributed systems. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods, Lecture Notes in Computer Science, vol. 8442, pp. 179\u2013193. Springer, Berlin (2014). doi:\n                        10.1007\/978-3-319-06410-9_13","DOI":"10.1007\/978-3-319-06410-9_13"},{"key":"280_CR17","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: Proceedings of the IEEE Computer Society\u2019s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004 (MASCOTS 2004), pp. 76\u201383. IEEE Computer Society (2004). doi:\n                        10.1109\/MASCOT.2004.1348184","DOI":"10.1109\/MASCOT.2004.1348184"},{"issue":"2","key":"280_CR18","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R Ehlers","year":"2012","unstructured":"Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232\u2013262 (2012). doi:\n                        10.1007\/s10703-011-0137-x","journal-title":"Form. Methods Syst. Des."},{"key":"280_CR19","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Moldovan, D.: Sparse positional strategies for safety games. In: Peled, D., Schewe, S. (eds.) Proceedings First Workshop on Synthesis, Berkeley, California, 7th and 8th July 2012. Electronic Proceedings in Theoretical Computer Science, vol. 84, pp. 1\u201316. Open Publishing Association (2012). doi:\n                        10.4204\/EPTCS.84.1","DOI":"10.4204\/EPTCS.84.1"},{"key":"280_CR20","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BF01768705","volume":"8","author":"A Ehrenfeucht","year":"1979","unstructured":"Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8, 109\u2013113 (1979). doi:\n                        10.1007\/BF01768705","journal-title":"Int. J. Game Theory"},{"key":"280_CR21","doi-asserted-by":"publisher","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a Safraless compositional approach. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 8559, pp. 192\u2013208. Springer, Berlin (2014). doi:\n                        10.1007\/978-3-319-08867-9_13","DOI":"10.1007\/978-3-319-08867-9_13"},{"issue":"5","key":"280_CR22","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5), 519\u2013539 (2012). doi:\n                        10.1007\/s10009-012-0228-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"280_CR23","doi-asserted-by":"publisher","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 2102, pp. 53\u201365. Springer, Berlin (2001). doi:\n                        10.1007\/3-540-44585-4_6","DOI":"10.1007\/3-540-44585-4_6"},{"key":"280_CR24","doi-asserted-by":"publisher","unstructured":"Hagihara, S., Egawa, N., Shimakawa, M., Yonezaki, N.: Minimal strongly unsatisfiable subsets of reactive system specifications. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering, ASE \u201914, pp. 629\u2013634. ACM, New York (2014). doi:\n                        10.1145\/2642937.2642968","DOI":"10.1145\/2642937.2642968"},{"key":"280_CR25","doi-asserted-by":"publisher","unstructured":"Hagihara, S., Kitamura, Y., Shimakawa, M., Yonezaki, N.: Extracting environmental constraints to make reactive system specifications realizable. In: 2009 16th Asia-Pacific Software Engineering Conference, pp. 61\u201368 (2009). doi:\n                        10.1109\/APSEC.2009.70","DOI":"10.1109\/APSEC.2009.70"},{"key":"280_CR26","doi-asserted-by":"publisher","unstructured":"Hagihara, S., Ueno, A., Tomita, T., Shimakawa, M., Yonezaki, N.: Simple synthesis of reactive systems with tolerance for unexpected environmental behavior. In: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE \u201916, pp. 15\u201321. ACM, New York (2016). doi:\n                        10.1145\/2897667.2897672","DOI":"10.1145\/2897667.2897672"},{"key":"280_CR27","doi-asserted-by":"publisher","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design, 2006. FMCAD \u201906, pp. 117 \u2013124 (2006). doi:\n                        10.1109\/FMCAD.2006.22","DOI":"10.1109\/FMCAD.2006.22"},{"key":"280_CR28","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science, 2005. FOCS 2005, pp. 531\u2013540 (2005). doi:\n                        10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"280_CR29","doi-asserted-by":"publisher","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, Hard and Soft Constraints, Frontiers in Artificial Intelligence and Applications, vol. 185, chap.\u00a019, pp. 613\u2013631. IOS Press, Amsterdam (2009). doi:\n                        10.3233\/978-1-58603-929-5-613","DOI":"10.3233\/978-1-58603-929-5-613"},{"key":"280_CR30","doi-asserted-by":"publisher","unstructured":"Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: 2011 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 43\u201350 (2011). doi:\n                        10.1109\/MEMCOD.2011.5970509","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"280_CR31","first-page":"407","volume-title":"Information Modelling and Knowledge Bases IV, Frontiers in Artificial Intelligence and Applications","author":"R Mori","year":"1993","unstructured":"Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Kangassalo, H., Jaakkola, H., Hori, K., Kitahashi, T. (eds.) Information Modelling and Knowledge Bases IV, Frontiers in Artificial Intelligence and Applications, vol. 16, pp. 407\u2013424. IOS Press, Amsterdam (1993)"},{"key":"280_CR32","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: 21st Annual IEEE Symposium on Logic in Computer Science, 2006, pp. 255\u2013264 (2006). doi:\n                        10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"280_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46 \u201357 (1977). doi:\n                        10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"280_CR34","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201989, pp. 179\u2013190. ACM, New York (1989). doi:\n                        10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"280_CR35","unstructured":"Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)"},{"key":"280_CR36","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega automata. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, SFCS \u201988, pp. 319\u2013327. IEEE Computer Society, Washington, DC (1988). doi:\n                        10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"280_CR37","doi-asserted-by":"publisher","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: de\u00a0Alfaro, L. (ed.) Foundations of Software Science and Computational Structures, Lecture Notes in Computer Science, vol. 5504, pp. 167\u2013181. Springer, Berlin (2009). doi:\n                        10.1007\/978-3-642-00596-1_13","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"280_CR38","doi-asserted-by":"publisher","unstructured":"Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In: Chakraborty, S., Mukund, M. (eds.) Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, pp. 42\u201356. Springer, Berlin (2012). doi:\n                        10.1007\/978-3-642-33386-6_5","DOI":"10.1007\/978-3-642-33386-6_5"},{"key":"280_CR39","doi-asserted-by":"publisher","unstructured":"Tomita, T., Hiura, S., Hagihara, S., Yonezaki, N.: A temporal logic with mean-payoff constraints. In: Aoki, T., Taguchi, K. (eds.) Formal Methods and Software Engineering, Lecture Notes in Computer Science, vol. 7635, pp. 249\u2013265. Springer, Berlin (2012). doi:\n                        10.1007\/978-3-642-34281-3_19","DOI":"10.1007\/978-3-642-34281-3_19"},{"key":"280_CR40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"280_CR41","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse 119\u2013136 (1985)"},{"issue":"1\u20132","key":"280_CR42","doi-asserted-by":"publisher","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\u20132), 343\u2013359 (1996). doi:\n                        10.1016\/0304-3975(95)00188-3","journal-title":"Theor. Comput. Sci."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0280-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0280-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0280-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T07:34:10Z","timestamp":1507793650000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0280-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,7]]},"references-count":42,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["280"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0280-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,7]]}}}