{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T20:10:25Z","timestamp":1742415025133,"version":"3.40.1"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,2,3]],"date-time":"2012-02-03T00:00:00Z","timestamp":1328227200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0224-3","type":"journal-article","created":{"date-parts":[[2012,2,2]],"date-time":"2012-02-02T19:47:02Z","timestamp":1328212022000},"page":"433-454","source":"Crossref","is-referenced-by-count":19,"title":["Safety first: a two-stage algorithm for the synthesis of reactive systems"],"prefix":"10.1007","volume":"15","author":[{"given":"Saqib","family":"Sohail","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,2,3]]},"reference":[{"key":"224_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, 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"224_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern B., Schneider F.B.: Recognizing safety and liveness. Distrib. Comput. 2, 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"224_CR3","first-page":"428","volume-title":"Eighth Conference on Computer Aided Verification (CAV\u201996) LNCS vol 1102.","author":"R.K. Brayton","year":"1996","unstructured":"Brayton R.K. et\u00a0al.: VIS: a system for verification and synthesis. In: Henzinger, T., Alur, R. (eds) Eighth Conference on Computer Aided Verification (CAV\u201996) LNCS vol 1102., pp. 428\u2013432. Springer, Rutgers University (1996)"},{"key":"224_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"224_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware form PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification 2007. Electronic Notes in Theoretical Computer Science. http:\/\/www.entcs.org\/","DOI":"10.1016\/j.entcs.2007.09.004"},{"issue":"3","key":"224_CR6","doi-asserted-by":"crossref","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. RAIRO Theor. Inf. Appl. 36(3), 261\u2013275 (2002)","journal-title":"RAIRO Theor. Inf. Appl."},{"key":"224_CR7","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"key":"224_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: 10th International Conference on Foundations of Software Science and Computation Structures. LNCS, vol. 4423, pp. 153\u2013167. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71389-0_12"},{"key":"224_CR9","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1051\/ita:1999129","volume":"33","author":"O. Carton","year":"1999","unstructured":"Carton O., Maceiras R.: Computing the Rabin index of a parity automaton. Theor. Inf. Appl. 33, 495\u2013505 (1999)","journal-title":"Theor. Inf. Appl."},{"key":"224_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"224_CR11","doi-asserted-by":"crossref","unstructured":"Emmanuel, F., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of the 21st International Conference on Computer Aided Verification, pp. 263\u2013277 (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"224_CR12","doi-asserted-by":"crossref","unstructured":"Filiot, Emmanuel, Jin, Nayiong, Raskin, Jean-Fran\u00e7ois: Compositional algorithms for LTL synthesis. In Proceedings of the 8th international conference on Automated technology for verification and analysis. LNCS, vol. 6252, pp. 112\u2013127, 2010","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"224_CR13","doi-asserted-by":"crossref","unstructured":"Godhal, Y., Chatterjee, K., Henzinger, T.: Synthesis of amba ahb from formal specification: a case study. Int. J. Softw. Tools Technol. Transf. (STTT), 1\u201317, (2011)","DOI":"10.1007\/s10009-011-0207-9"},{"key":"224_CR14","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, London (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"224_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Kupferman, O., Rajamani, S.: Fair simulation. In: Proceedings of the 9th International Conference on Concurrency Theory (CONCUR\u201997). LNCS, vol. 1243, pp. 273\u2013287. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63141-0_19"},{"key":"224_CR16","unstructured":"Horn, F.: Streett games on finite graphs. In: Workshop on Games in Design and Verification Edimburgh, UK, July 2005"},{"key":"224_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Piterman, N.: Solving games without determinization. In: 15th Conference on Computer Science Logic, Szeged, Hungary. LNCS, vol. 4207, pp. 394\u2013409 (2006)","DOI":"10.1007\/11874683_26"},{"key":"224_CR18","doi-asserted-by":"crossref","unstructured":"Harding, A., Ryan, M., Schobbens, P.Y.: A new algorithm for strategy synthesis in LTL games. In: Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, UK. LNCS, vol. 3440, pp. 477\u2013492 (2005)","DOI":"10.1007\/978-3-540-31980-1_31"},{"key":"224_CR19","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, Miami, FL, pp. 117\u2013123 (2006)","DOI":"10.1145\/1109557.1109571"},{"key":"224_CR20","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France. LNCS, vol. 1770, pp. 290\u2013301. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46541-3_24"},{"key":"224_CR21","doi-asserted-by":"crossref","unstructured":"Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Barner, S., Kroening, D., Raz, O. (eds) Proceeding of the 6th International Haifa Verification Conference (HVC \u201910). LNCS, vol. 6504, pp. 161\u2013181 (2011)","DOI":"10.1007\/978-3-642-19583-9_16"},{"key":"224_CR22","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Eighteenth Conference on Computer Aided Verification. LNCS, vol. 4144, pp. 31\u201344 (2006)","DOI":"10.1007\/11817963_6"},{"key":"224_CR23","first-page":"172","volume-title":"Eleventh Conference on Computer Aided Verification (CAV\u201999) LNCS vol 1633.","author":"O. Kupferman","year":"1999","unstructured":"Kupferman O., Vardi M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds) Eleventh Conference on Computer Aided Verification (CAV\u201999) LNCS vol 1633., pp. 172\u2013183. Springer, Berlin (1999)"},{"key":"224_CR24","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Foundations of Computer Science, Pittsburgh, PA, pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"224_CR25","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of \u03c9-automata. In: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, 1999. LNCS, vol. 1738 (1999)","DOI":"10.1007\/3-540-46691-6_8"},{"issue":"4","key":"224_CR26","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber L.H.: Decision problems for \u03c9-automata. Math. Syst. Theory 3(4), 376\u2013384 (1969)","journal-title":"Math. Syst. Theory"},{"key":"224_CR27","doi-asserted-by":"crossref","unstructured":"Lindner, T.: Case Study \u201cProduction Cell\u201d: A Comparative Study in Formal Software Development, chap. 2, pp. 9\u201321. FZI (1994)","DOI":"10.1007\/3-540-58867-1_47"},{"key":"224_CR28","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"224_CR29","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Theoretical Computer Science (TCS 2000). LNCS, vol. 1872, pp. 521\u2013535. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44929-9_36"},{"key":"224_CR30","doi-asserted-by":"crossref","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D.A. Martin","year":"1975","unstructured":"Martin D.A.: Borel determinacy. Ann. Math. Second Ser. 102, 363\u2013371 (1975)","journal-title":"Ann. Math. Second Ser."},{"key":"224_CR31","doi-asserted-by":"crossref","unstructured":"Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) Computation Theory. LNCS, vol. 208, pp. 157\u2013168. Springer, Berlin (1984)","DOI":"10.1007\/3-540-16066-3_15"},{"key":"224_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, pp. 377\u2013410 (1990)","DOI":"10.1145\/93385.93442"},{"key":"224_CR33","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Games, Automata, Logics, and Formal Verification (GandALF). Electronic Proceedings in Theoretical Computer Science (EPTCS), Minori, Italy, vol. 25, pp. 89\u2013102 (2010)","DOI":"10.4204\/EPTCS.25.11"},{"key":"224_CR34","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/0304-3975(92)90076-R","volume":"97","author":"D.E. Muller","year":"1992","unstructured":"Muller D.E., Saoudi A., Schupp P.: Alternating automata, the weak monadic theory of trees and its complexity. Theor. Comput. Sci. 97, 233\u2013244 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"224_CR35","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: 21st Symposium on Logic in Computer Science, Seattle, WA, pp. 255\u2013264 (2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"224_CR36","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u00e1r, Y.: Synthesis of reactive(1) designs. In: 7th International Conference on Verification, Model Checking and Abstract Interpretation. LNCS, vol. 3855, pp. 364\u2013380. Springer, Berlin (2006)","DOI":"10.1007\/11609773_24"},{"key":"224_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of Symposium on Principles of Programming Languages (POPL \u201989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"224_CR38","unstructured":"Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, March 1989"},{"key":"224_CR39","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) Twelfth Conference on Computer Aided Verification (CAV\u201900). LNCS, vol. 1855, pp. 248\u2013263. Springer, Berlin (2000)","DOI":"10.1007\/10722167_21"},{"key":"224_CR40","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"D. Scott","year":"1959","unstructured":"Scott D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"224_CR41","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6, 495\u2013511 (1994)","journal-title":"Formal Aspects Comput."},{"key":"224_CR42","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F., Ravi, K.: A hybrid algorithm for LTL games. In: Verification, Model Checking and Abstract Interpretation, San Francisco, CA. LNCS, vol. 4905, pp. 309\u2013323 (2008)","DOI":"10.1007\/978-3-540-78163-9_26"},{"key":"224_CR43","doi-asserted-by":"crossref","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 900, pp. 1\u201313. Springer, Berlin (1995)","DOI":"10.1007\/3-540-59042-0_57"},{"key":"224_CR44","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"issue":"1\u20132","key":"224_CR45","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0224-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0224-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0224-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T19:30:26Z","timestamp":1742412626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0224-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,3]]},"references-count":45,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["224"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0224-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,2,3]]}}}