{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T23:24:31Z","timestamp":1781565871534,"version":"3.54.5"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,8,11]],"date-time":"2023-08-11T00:00:00Z","timestamp":1691712000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,8,11]],"date-time":"2023-08-11T00:00:00Z","timestamp":1691712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100008252","name":"Universit\u00e0 degli Studi di Udine","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008252","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (\u00a0) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response \u00a0(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {LTL} _{\\textsf {EBR} }\\textsf {{+}P} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>LTL<\/mml:mi><mml:mi>EBR<\/mml:mi><\/mml:msub><mml:mo>+<\/mml:mo><mml:mi>P<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0for short) has been introduced. It allows one to express safety languages definable in \u00a0and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce -\u00a0, an extension of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {LTL} _{\\textsf {EBR} }\\textsf {{+}P} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>LTL<\/mml:mi><mml:mi>EBR<\/mml:mi><\/mml:msub><mml:mo>+<\/mml:mo><mml:mi>P<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {LTL} _{\\textsf {EBR} }\\textsf {{+}P} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>LTL<\/mml:mi><mml:mi>EBR<\/mml:mi><\/mml:msub><mml:mo>+<\/mml:mo><mml:mi>P<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0in practice. Second, we the expressiveness of -\u00a0starting from the expressiveness of its fragments. In particular, we prove that: (1)<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {LTL} _{\\textsf {EBR} }\\textsf {{+}P} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>LTL<\/mml:mi><mml:mi>EBR<\/mml:mi><\/mml:msub><mml:mo>+<\/mml:mo><mml:mi>P<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0is expressively complete with respect to the safety fragment of \u00a0, (2) the removal of past operators from<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {LTL} _{\\textsf {EBR} }\\textsf {{+}P} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>LTL<\/mml:mi><mml:mi>EBR<\/mml:mi><\/mml:msub><mml:mo>+<\/mml:mo><mml:mi>P<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0results into a loss of expressive power, and (3) -\u00a0is expressively equivalent to the logic \u00a0of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from -\u00a0specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) \u00a0. The experimental evaluation shows promising results.<\/jats:p>","DOI":"10.1007\/s10270-023-01122-4","type":"journal-article","created":{"date-parts":[[2023,8,11]],"date-time":"2023-08-11T06:01:32Z","timestamp":1691733692000},"page":"427-453","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Fairness, assumptions, and guarantees for extended bounded response LTL+P\u00a0synthesis"],"prefix":"10.1007","volume":"23","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7125-787X","authenticated-orcid":false,"given":"Luca","family":"Geatti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicola","family":"Gigante","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,8,11]]},"reference":[{"key":"1122_CR1","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S.: Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis. In: Calinescu, R., Pasareanu, C.S. (eds.) Software Engineering and Formal Methods\u201419th International Conference, SEFM 2021, Virtual Event, December 6\u201310, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13085, pp. 351\u2013371. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_20","DOI":"10.1007\/978-3-030-92124-8_20"},{"key":"1122_CR2","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S.: Expressiveness of Extended Bounded Response LTL, vol. 346, pp. 152\u2013165 (2021). https:\/\/doi.org\/10.4204\/EPTCS.346.10","DOI":"10.4204\/EPTCS.346.10"},{"key":"1122_CR3","unstructured":"Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, vol. 1962, pp. 23\u201335 (1962)"},{"key":"1122_CR4","doi-asserted-by":"publisher","unstructured":"Buchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. In: The Collected Works of J. Richard B\u00fcchi, pp. 525\u2013541. Springer (1990). https:\/\/doi.org\/10.1016\/S0019-9958(66)80013-X","DOI":"10.1016\/S0019-9958(66)80013-X"},{"key":"1122_CR5","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: International Colloquium on Automata, Languages, and Programming (ICALP), pp. 652\u2013671. Springer (1989). https:\/\/doi.org\/10.1016\/0022-0000(86)90026-7","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"1122_CR6","unstructured":"Rosner, R.: Modular synthesis of reactive systems. PhD thesis, PhD thesis, Weizmann Institute of Science (1992)"},{"issue":"3","key":"1122_CR7","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., Saar, Y.: Synthesis of reactive (1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"1122_CR8","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A Symbolic Approach to Safety LTL Synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) Proceedings of the 13th International Haifa Verification Conference. Lecture Notes in Computer Science, vol. 10629, pp. 147\u2013162. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10","DOI":"10.1007\/978-3-319-70389-3_10"},{"key":"1122_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S.: Extended bounded response LTL: a new safety fragment for efficient reactive synthesis. In: Formal Methods in System Design, pp. 1\u201349. Springer (2021)","DOI":"10.1007\/s10703-021-00383-3"},{"key":"1122_CR10","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: Sat-based synthesis methods for safety specs. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 1\u201320. Springer (2014)","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"1122_CR11","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 52\u201359. IEEE (2012)"},{"issue":"2","key":"1122_CR12","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electron. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"5\u20136","key":"1122_CR13","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5\u20136), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1122_CR14","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual Symposium on Foundations of Computer Science (FOCS), pp. 531\u2013540. IEEE (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"1122_CR15","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 354\u2013370. Springer (2017)","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"1122_CR16","doi-asserted-by":"publisher","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Workshop on Logic of Programs, pp. 196\u2013218. Springer (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_16","DOI":"10.1007\/3-540-15648-8_16"},{"key":"1122_CR17","doi-asserted-by":"publisher","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds.) Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980, pp. 163\u2013173. ACM Press (1980). https:\/\/doi.org\/10.1145\/567446.567462","DOI":"10.1145\/567446.567462"},{"key":"1122_CR18","unstructured":"Markey, N.: Temporal logic with past is exponentially more succinct (2003)"},{"issue":"1","key":"1122_CR19","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/568438.568455","volume":"32","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. ACM SIGACT News 32(1), 60\u201365 (2001). https:\/\/doi.org\/10.1145\/568438.568455","journal-title":"ACM SIGACT News"},{"issue":"1\u20136","key":"1122_CR20","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Math. Log. Q. 6(1\u20136), 66\u201392 (1960). https:\/\/doi.org\/10.1002\/malq.19600060105","journal-title":"Math. Log. Q."},{"key":"1122_CR21","unstructured":"BUCHI, J.: On a decision method in restricted second-order arithmetics. In: Proceedings of International Congress on Logic, Methodology and Philosophy of Science (1960). Stanford Univ. Press"},{"issue":"3","key":"1122_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001). https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Formal Methods Syst. Des."},{"key":"1122_CR23","volume-title":"Counter-Free Automata (MIT Research Monograph No. 65)","author":"R McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT Research Monograph No. 65). The MIT Press (1971)"},{"issue":"21","key":"1122_CR24","doi-asserted-by":"publisher","first-page":"403","DOI":"10.4064\/-21-1-403-417","volume":"1","author":"W Thomas","year":"1988","unstructured":"Thomas, W.: Safety-and liveness-properties in propositional temporal logic: characterizations and decidability. Banach Center Publ. 1(21), 403\u2013417 (1988). https:\/\/doi.org\/10.4064\/-21-1-403-417","journal-title":"Banach Center Publ."},{"key":"1122_CR25","doi-asserted-by":"publisher","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, pp. 474\u2013486. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_97","DOI":"10.1007\/3-540-55719-9_97"},{"issue":"5","key":"1122_CR26","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495\u2013511 (1994). https:\/\/doi.org\/10.1007\/BF01211865","journal-title":"Formal Aspects Comput."},{"key":"1122_CR27","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing, pp. 377\u2013410 (1990). https:\/\/doi.org\/10.1145\/93385.93442","DOI":"10.1145\/93385.93442"},{"issue":"1","key":"1122_CR28","doi-asserted-by":"publisher","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), 1\u201337 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1092","journal-title":"Inf. Comput."},{"key":"1122_CR29","doi-asserted-by":"publisher","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: International Conference on Computer Aided Verification (CAV), pp. 263\u2013277. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_6","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"1122_CR30","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: Proceedings of 29th IEEE Symposium on Foundation of Computer Science, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"1122_CR31","doi-asserted-by":"publisher","unstructured":"Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using muller conditions. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12\u201316, 2021, Glasgow, Scotland (Virtual Conference). LIPIcs, vol. 198, pp. 123\u2013112314. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.123","DOI":"10.4230\/LIPIcs.ICALP.2021.123"},{"key":"1122_CR32","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), pp. 141\u2013154. IEEE (2000)","DOI":"10.1109\/LICS.2000.855763"},{"issue":"3","key":"1122_CR33","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L De Alfaro","year":"2007","unstructured":"De Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theoret. Comput. Sci. 386(3), 188\u2013217 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.07.008","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"1122_CR34","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.entcs.2013.07.009","volume":"19","author":"S Jacobs","year":"2017","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., K\u00f6nighofer, R., P\u00e9rez, G.A., Raskin, J.-F., Ryzhyk, L., Sankur, O., et al.: The first reactive synthesis competition (syntcomp 2014). Int. J. Softw. Tools Technol. Transfer 19(3), 367\u2013390 (2017). https:\/\/doi.org\/10.1016\/j.entcs.2013.07.009","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1122_CR35","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. In: International Conference on Computer Aided Verification, pp. 95\u2013107. Springer (2007). https:\/\/doi.org\/10.1023\/A:1008734703554","DOI":"10.1023\/A:1008734703554"},{"key":"1122_CR36","first-page":"1","volume-title":"The smv Language","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: The smv Language, pp. 1\u201349. Cadence Berkeley Labs, London (1999)"},{"key":"1122_CR37","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: International Conference on Computer Aided Verification (CAV), pp. 410\u2013424. Springer (2010). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","DOI":"10.1016\/S0304-3975(98)00009-7"},{"key":"1122_CR38","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: ACTL $$\\cap $$ LTL synthesis. In: International Conference on Computer Aided Verification (CAV), pp. 39\u201354. Springer (2012). https:\/\/doi.org\/10.1007\/11609773_24","DOI":"10.1007\/11609773_24"},{"key":"1122_CR39","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S.: Reactive synthesis from extended bounded response LTL specifications. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21\u201324, 2020, pp. 83\u201392. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_15","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_15"},{"key":"1122_CR40","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 364\u2013380. Springer (2006)","DOI":"10.1007\/11609773_24"},{"key":"1122_CR41","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"1122_CR42","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O.: Gr (1) synthesis for ltl specification patterns. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 96\u2013106 (2015)","DOI":"10.1145\/2786805.2786824"},{"key":"1122_CR43","doi-asserted-by":"crossref","unstructured":"Ehlers, R., Raman, V.: Slugs: Extensible GR(1) synthesis. In: International Conference on Computer Aided Verification, pp. 333\u2013339. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_18"},{"issue":"5","key":"1122_CR44","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1007\/s10270-021-00868-z","volume":"20","author":"S Maoz","year":"2021","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021)","journal-title":"Softw. Syst. Model."},{"key":"1122_CR45","doi-asserted-by":"crossref","unstructured":"Cavezza, D.G., Alrajeh, D., Gy\u00f6rgy, A.: Minimal assumptions refinement for realizable specifications. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, pp. 66\u201376 (2020)","DOI":"10.1145\/3372020.3391557"},{"key":"1122_CR46","doi-asserted-by":"publisher","unstructured":"Morgenstern, A., Schneider, K.: A LTL fragment for GR(1)-synthesis. In: Reich, J., Finkbeiner, B. (eds.) Proceedings International Workshop on Interactions, Games and Protocols, iWIGP 2011, Saarbr\u00fccken, Germany, 27th March 2011. EPTCS, vol. 50, pp. 33\u201345 (2011). https:\/\/doi.org\/10.4204\/EPTCS.50.3","DOI":"10.4204\/EPTCS.50.3"},{"key":"1122_CR47","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: International Conference on Computer Aided Verification (CAV), pp. 365\u2013379. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_33","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"1122_CR48","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: An experimentation framework for bounded synthesis. In: International Conference on Computer Aided Verification (CAV), pp. 325\u2013332. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"1122_CR49","doi-asserted-by":"crossref","unstructured":"Babiak, T., K\u0159et\u00ednsk\u1ef3, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: Ltl to b\u00fcchi automata translation: Fast and more deterministic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 95\u2013109. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"1122_CR50","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 122\u2013129. Springer (2016). https:\/\/doi.org\/10.1007\/3-540-60915-6_6","DOI":"10.1007\/3-540-60915-6_6"},{"key":"1122_CR51","unstructured":"Jacobs, S., Bloem, R.: The 5th reactive synthesis competition (SYNTCOMP 2018)"},{"key":"1122_CR52","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: Aiger 1.9 and beyond (2011). Available at fmv. jku.at\/hwmcc11\/beyond1. pdf"},{"key":"1122_CR53","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: International Conference on Computer Aided Verification (CAV), pp. 289\u2013306. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"1122_CR54","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00236-019-00349-3","volume":"57","author":"M Luttenberger","year":"2020","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from ltl specifications via parity games. Acta Informatica 57(1), 3\u201336 (2020)","journal-title":"Acta Informatica"},{"key":"1122_CR55","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: International Conference on Computer Aided Verification, pp. 578\u2013586. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"1122_CR56","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis\u201416th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 543\u2013550. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34","DOI":"10.1007\/978-3-030-01090-4_34"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01122-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-023-01122-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01122-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T01:16:47Z","timestamp":1729905407000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-023-01122-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,11]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["1122"],"URL":"https:\/\/doi.org\/10.1007\/s10270-023-01122-4","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,11]]},"assertion":[{"value":"3 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 July 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 July 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}