{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:56:01Z","timestamp":1757314561222},"publisher-location":"Berlin, Heidelberg","reference-count":54,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_62","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"883-889","source":"Crossref","is-referenced-by-count":24,"title":["GOAL for Games, Omega-Automata, and Logics"],"prefix":"10.1007","author":[{"given":"Ming-Hsien","family":"Tsai","sequence":"first","affiliation":[]},{"given":"Yih-Kuen","family":"Tsay","sequence":"additional","affiliation":[]},{"given":"Yu-Shiang","family":"Hwang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"62_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-14295-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Clemente, L., Hol\u00edk, L., Hong, C.-D., Mayr, R., Vojnar, T.: Simulation subsumption in Ramsey-based B\u00fcchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 132\u2013147. Springer, Heidelberg (2010)"},{"issue":"2","key":"62_CR2","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.tcs.2006.07.026","volume":"363","author":"C.S. Althoff","year":"2006","unstructured":"Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of B\u00fcchi automata. TCS\u00a0363(2), 224\u2013233 (2006)","journal-title":"TCS"},{"key":"62_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Weiss, G.: RTComposer: a framework for real-time components with scheduling interfaces. In: EMSOFT, pp. 159\u2013168. ACM (2008)","DOI":"10.1145\/1450058.1450080"},{"key":"62_CR4","doi-asserted-by":"crossref","unstructured":"Boker, U., Kupferman, O.: Co-ing B\u00fcchi made tight and useful. In: LICS, pp. 245\u2013254. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.32"},{"key":"62_CR5","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: CLMPS, pp. 1\u201312. Stanford University Press (1962)"},{"issue":"6","key":"62_CR6","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. Informatique Th\u00e9orique et Applications\u00a033(6), 495\u2013506 (1999)","journal-title":"Informatique Th\u00e9orique et Applications"},{"key":"62_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-45138-9_26","volume-title":"Mathematical Foundations of Computer Science 2003","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 318\u2013327. Springer, Heidelberg (2003)"},{"key":"62_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-19835-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Chatterjee","year":"2011","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: Quantitative synthesis tool. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 267\u2013271. Springer, Heidelberg (2011)"},{"key":"62_CR9","doi-asserted-by":"crossref","unstructured":"Cicho\u0144, J., Czubak, A., Jasi\u0144ski, A.: Minimal B\u00fcchi automata for certain classes of LTL formulas. In: DepCos-RELCOMEX, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/DepCoS-RELCOMEX.2009.31"},{"key":"62_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"62_CR11","unstructured":"Diekert, V., Gastin, P.: First-order definable languages. In: Logic and Automata. Texts in Logic and Games, vol.\u00a02, pp. 261\u2013306. Amsterdam Univ. Press (2008)"},{"issue":"5","key":"62_CR12","doi-asserted-by":"crossref","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SICOMP\u00a034(5), 1159\u20131175 (2005)","journal-title":"SICOMP"},{"key":"62_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-04761-9_15","volume-title":"Automated Technology for Verification and Analysis","author":"O. Friedmann","year":"2009","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 182\u2013196. Springer, Heidelberg (2009)"},{"key":"62_CR14","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"62_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-540-45138-9_38","volume-title":"Mathematical Foundations of Computer Science 2003","author":"P. Gastin","year":"2003","unstructured":"Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 439\u2013448. Springer, Heidelberg (2003)"},{"key":"62_CR16","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: PSTV, pp. 3\u201318. Chapman & Hall (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"62_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"issue":"3","key":"62_CR18","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. TOPLAS\u00a016(3), 843\u2013871 (1994)","journal-title":"TOPLAS"},{"key":"62_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","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, pp. 610\u2013624. Springer, Heidelberg (2002)"},{"key":"62_CR20","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (September 2003)"},{"key":"62_CR21","unstructured":"IEEE standard for property specification language (PSL). IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005), 1\u2013182 (2010)"},{"key":"62_CR22","unstructured":"Java Plugin Framework, \n                    \n                      http:\/\/jpf.sourceforge.net"},{"key":"62_CR23","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)"},{"issue":"4","key":"62_CR24","doi-asserted-by":"crossref","first-page":"1519","DOI":"10.1137\/070686652","volume":"38","author":"M. Jurdzi\u0144ski","year":"2008","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SICOMP\u00a038(4), 1519\u20131532 (2008)","journal-title":"SICOMP"},{"key":"62_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","volume-title":"Automata, Languages and Programming","author":"D. K\u00e4hler","year":"2008","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol.\u00a05125, pp. 724\u2013735. Springer, Heidelberg (2008)"},{"key":"62_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 97\u2013109. Springer, Heidelberg (1993)"},{"issue":"1","key":"62_CR27","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"issue":"5","key":"62_CR28","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1093\/logcom\/12.5.701","volume":"12","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A.: Complete proof system for QPTL. Journal of Logic and Computation\u00a012(5), 701\u2013745 (2002)","journal-title":"Journal of Logic and Computation"},{"key":"62_CR29","doi-asserted-by":"crossref","unstructured":"Klotz, T., Se\u00dfler, N., Straube, B., Fordran, E.: Compositional verification of material handling systems. In: ETFA, pp. 1\u20138. IEEE (2012)","DOI":"10.1109\/CoASE.2012.6386358"},{"issue":"3","key":"62_CR30","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. TOCL\u00a02(3), 408\u2013429 (2001)","journal-title":"TOCL"},{"issue":"1","key":"62_CR31","first-page":"59","volume":"35","author":"R.P. Kurshan","year":"1987","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. JCSS\u00a035(1), 59\u201371 (1987)","journal-title":"JCSS"},{"key":"62_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-36387-4_6","volume-title":"Automata, Logics, and Infinite Games","author":"R. K\u00fcsters","year":"2002","unstructured":"K\u00fcsters, R.: Memoryless determinacy of parity games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 95\u2013106. Springer, Heidelberg (2002)"},{"issue":"4","key":"62_CR33","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for omega-automata. Mathematical Systems Theory\u00a03(4), 376\u2013384 (1969)","journal-title":"Mathematical Systems Theory"},{"key":"62_CR34","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377\u2013410 (1990)","DOI":"10.1145\/93385.93442"},{"key":"62_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4_2","volume-title":"Automata, Logics, and Infinite Games","author":"R. Mazala","year":"2002","unstructured":"Mazala, R.: Infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 23\u201338. Springer, Heidelberg (2002)"},{"issue":"2","key":"62_CR36","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(2), 149\u2013184 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1&2","key":"62_CR37","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS\u00a0141(1&2), 69\u2013107 (1995)","journal-title":"TCS"},{"key":"62_CR38","unstructured":"Peng, H., Mokhtari, Y., Tahar, S.: Environment synthesis for compositional model checking. In: ICCD, pp. 70\u201375. IEEE Computer Society (2002)"},{"issue":"3","key":"62_CR39","first-page":"5","volume":"3","author":"N. Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. LMCS\u00a03(3), paper 5 (2007)","journal-title":"LMCS"},{"key":"62_CR40","unstructured":"Rodger, S., Finley, T.: JFLAP, \n                    \n                      http:\/\/www.jflap.org\/"},{"key":"62_CR41","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: FOCS, pp. 319\u2013327. IEEE (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"62_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-540-77050-3_37","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"S. Schewe","year":"2007","unstructured":"Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 449\u2013460. Springer, Heidelberg (2007)"},{"key":"62_CR43","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS. LIPIcs, vol.\u00a03, pp. 661\u2013672 (2009)"},{"key":"62_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: \u201cMore\u201d deterministic 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":"62_CR45","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with appplications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"62_CR46","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games. In: FMCAD, pp. 77\u201384. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351138"},{"key":"62_CR47","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":"62_CR48","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Complementation of B\u00fcchi automata revisited. In: Jewels are Forever, pp. 109\u2013120. Springer (1999)","DOI":"10.1007\/978-3-642-60207-8_10"},{"key":"62_CR49","unstructured":"Tsai, M.-H., Chan, W.-C., Tsay, Y.-K., Luo, C.-J.: Incremental translation of full PTL formulae to B\u00fcchi automata (manuscript 2013)"},{"key":"62_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-18098-9_28","volume-title":"Implementation and Application of Automata","author":"M.-H. Tsai","year":"2011","unstructured":"Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of B\u00fcchi complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol.\u00a06482, pp. 261\u2013271. Springer, Heidelberg (2011)"},{"key":"62_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-78800-3_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2008","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 346\u2013350. Springer, Heidelberg (2008)"},{"key":"62_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-71209-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2007","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A graphical tool for manipulating B\u00fcchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 466\u2013471. Springer, Heidelberg (2007)"},{"issue":"2","key":"62_CR53","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10009-012-0268-4","volume":"15","author":"Y.-K. Tsay","year":"2013","unstructured":"Tsay, Y.-K., Tsai, M.-H., Chang, J.-S., Chang, Y.-W., Liu, C.-S.: B\u00fcchi Store: An open repository of \u03c9-automata. STTT\u00a015(2), 109\u2013123 (2013)","journal-title":"STTT"},{"issue":"1-2","key":"62_CR54","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. TCS\u00a0200(1-2), 135\u2013183 (1998)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_62","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:33:59Z","timestamp":1557930839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}