{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:49:00Z","timestamp":1725504540583},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_26","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"309-323","source":"Crossref","is-referenced-by-count":13,"title":["A Hybrid Algorithm for LTL Games"],"prefix":"10.1007","author":[{"given":"Saqib","family":"Sohail","sequence":"first","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]},{"given":"Kavita","family":"Ravi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1007\/3-540-36494-3_58","volume-title":"STACS 2003","author":"H. Bj\u00f6rklund","year":"2003","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.: A discrete subexponential algorithm for parity games. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 663\u2013674. Springer, Heidelberg (2003)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-40922-X_4","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Bloem","year":"2000","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n logn symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 37\u201354. Springer, Heidelberg (2000)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al.: Specify, compile, run: Hardware form PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification. Electronic Notes in Theoretical Computer Science (2007), http:\/\/www.entcs.org\/","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., et al.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"issue":"8","key":"26_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers\u00a0C"},{"key":"26_CR6","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":"26_CR7","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc.\u00a0138, 295\u2013311 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-61042-1_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Buhrke","year":"1996","unstructured":"Buhrke, N., Lescow, H., V\u00f6ge, J.: Strategy construction in infinite games with Streett and Rabin chain winning conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 207\u2013225. Springer, Heidelberg (1996)"},{"key":"26_CR9","doi-asserted-by":"publisher","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. Theoretical Informatics and Applications\u00a033, 495\u2013505 (1999)","journal-title":"Theoretical Informatics and Applications"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-71389-0_12","volume-title":"Foundations of Software Science and Computational Structures","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized Parity Games. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 153\u2013167. Springer, Heidelberg (2007)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-73368-3_13","volume-title":"Computer Aided Verification","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Faella, M.: Accelerated algorithms for 3-color parity games with an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 108\u2013120. Springer, Heidelberg (2007)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. 32nd IEEE Symposium on Foundations of Computer Science. pp. 368\u2013377 (October 1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_57","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2001","unstructured":"Etessami, K., Wilke, T., Schuller, A.: Fair Simulation Relations, Parity Games, and State Space Reduction for B\u00fcchi Automata. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, Springer, Heidelberg (2001)"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Computer Aided Verification","author":"D. Geist","year":"1994","unstructured":"Geist, D., Beer, I.: Efficient model checking by automated ordering of transition relation partitions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 299\u2013310. Springer, Heidelberg (1994)"},{"key":"26_CR16","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected componenets in a linear number of symbolic steps. In: Symposium on Discrete Algorithms, Baltimore, MD (January 2003)"},{"key":"26_CR17","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification","author":"S. Gurumurthy","year":"2002","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair Simulation Minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-540-31980-1_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Harding","year":"2005","unstructured":"Harding, A., Ryan, M., Schobbens, P.-Y.: A new algorithm for strategy synthesis in LTL games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 477\u2013492. Springer, Heidelberg (2005)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"CONCUR\u201997: Concurrency Theory","author":"T. Henzinger","year":"1997","unstructured":"Henzinger, T., Kupferman, O., Rajamani, S.: Fair simulation. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 273\u2013287. Springer, Heidelberg (1997)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11874683_26","volume-title":"Computer Science Logic","author":"T.A. Henzinger","year":"2006","unstructured":"Henzinger, T.A., Piterman, N.: Solving games without determinization. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 394\u2013409. Springer, Heidelberg (2006)"},{"key":"26_CR22","unstructured":"Horn, F.: Streett games on finite graphs. In: Workshop on Games in Design and Verification, Edimburgh, UK (July 2005)"},{"issue":"2","key":"26_CR23","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/s10009-004-0146-9","volume":"6","author":"H. Jin","year":"2004","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. Software Tools for Technology Transfer\u00a06(2), 102\u2013116 (2004)","journal-title":"Software Tools for Technology Transfer"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design (FMCAD 2006), San Jose, CA, pp. 117\u2013124 (November 2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M. Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"26_CR27","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 (January 2006)","DOI":"10.1145\/1109557.1109571"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Katz","year":"1999","unstructured":"Katz, S., Grumberg, O., Geist, D.: Have I written enough properties?\u201d \u2014 A method of comparison between specification and implementation. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 280\u2013297. Springer, Heidelberg (1999)"},{"key":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Foundations of Computer Science, Pittsburgh, PA, pp. 531\u2013542 (October 2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"26_CR31","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 (January 1985)","DOI":"10.1145\/318593.318622"},{"key":"26_CR32","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D.A. Martin","year":"1975","unstructured":"Martin, D.A.: Borel determinacy. Annals of Mathematics\u00a0102, 363\u2013371 (1975)","journal-title":"Annals of Mathematics"},{"key":"26_CR33","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1994","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1994)"},{"key":"26_CR34","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. Annals of Pure and Applied Logic\u00a065, 149\u2013184 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-40922-X_6","volume-title":"Formal Methods in Computer-Aided Design","author":"I.-H. Moon","year":"2000","unstructured":"Moon, I.-H., Hachtel, G.D., Somenzi, F.: Border-block triangular form and conjunction schedule in image computation. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 73\u201390. Springer, Heidelberg (2000)"},{"key":"26_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-16066-3_15","volume-title":"Computation Theory","author":"A.W. Mostowski","year":"1985","unstructured":"Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol.\u00a0208, pp. 157\u2013168. Springer, Heidelberg (1985)"},{"key":"26_CR37","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 (August 2006)","DOI":"10.1109\/LICS.2006.28"},{"key":"26_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u00b4ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"26_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"26_CR40","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. In: Regional Conference Series in Mathematics, American Mathematical Society, Providence (1972)","DOI":"10.1090\/cbms\/013"},{"key":"26_CR41","unstructured":"Ranjan, R.K., et al.: Efficient BDD algorithms for FSM synthesis and verification. In: Presented at IWLS 1995, Lake Tahoe, CA (May 1995)"},{"key":"26_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"key":"26_CR43","unstructured":"Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science (March 1989)"},{"key":"26_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: More deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"26_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"26_CR46","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control\u00a054, 121\u2013141 (1982)","journal-title":"Information and Control"},{"key":"26_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60275-5","volume-title":"STACS 95","author":"W. Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol.\u00a0900, pp. 1\u201313. Springer, Heidelberg (1995)"},{"issue":"2","key":"26_CR48","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0019-9958(79)90653-3","volume":"43","author":"K. Wagner","year":"1979","unstructured":"Wagner, K.: On \u03c9-regular sets. Information and Control\u00a043(2), 123\u2013177 (1979)","journal-title":"Information and Control"},{"key":"26_CR49","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":"26_CR50","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0200(1\u20132), 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:00:36Z","timestamp":1619521236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_26","relation":{},"subject":[]}}