{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:24:18Z","timestamp":1757312658524,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_10","type":"book-chapter","created":{"date-parts":[[2011,1,8]],"date-time":"2011-01-08T02:15:55Z","timestamp":1294452955000},"page":"96-110","source":"Crossref","is-referenced-by-count":29,"title":["On Complementing Nondeterministic B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Sankar","family":"Gurumurthy","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing\u00a02, 117\u2013126 (1987)","journal-title":"Distributed Computing"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 222\u2013235. Springer, Heidelberg (1999)"},{"unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: 1960 International Congress on Logic, Methodology, and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)","key":"10_CR5"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"K. Chandra","year":"1981","unstructured":"Chandra, K., Kozen, D.C., Stockmeyer, L.J.: Alternation. JACM\u00a028(1), 114\u2013133 (1981)","journal-title":"JACM"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-36206-1_15","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"C. Fritz","year":"2002","unstructured":"Fritz, C., Wilke, T.: State space reductions for alternating B\u00fcchi automata. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 157\u2013168. Springer, Heidelberg (2002)"},{"key":"10_CR8","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\u2013623. Springer, Heidelberg (2002)"},{"key":"10_CR9","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"doi-asserted-by":"crossref","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9-automata with application to temporal logic. In: FOCS, pp. 358\u2013367 (1991)","key":"10_CR10","DOI":"10.1109\/SFCS.1991.185391"},{"doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Relating linear and branching model checking. In: IFIP PROCOMET, pp. 304\u2013326 (1998)","key":"10_CR11","DOI":"10.1007\/978-0-387-35358-6_21"},{"issue":"3","key":"10_CR12","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. ACM TOCL\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM TOCL"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","volume":"35","author":"R.P. Kurshan","year":"1987","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. Journal of Computer and System Sciences\u00a035, 59\u201371 (1987)","journal-title":"Journal of Computer and System Sciences"},{"key":"10_CR14","volume-title":"Computer-AidedVerification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-AidedVerification of Coordinating Processes. Princeton University Press, Princeton (1994)"},{"doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107 (1985)","key":"10_CR15","DOI":"10.1145\/318593.318622"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-44929-9_36","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"C. L\u00f6ding","year":"2000","unstructured":"L\u00f6ding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 521\u2013535. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: FOCS, pp. 643\u2013652 (2000)","key":"10_CR17","DOI":"10.1109\/SFCS.2000.892332"},{"unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988) (manuscript)","key":"10_CR18"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. TCS\u00a032, 321\u2013330 (1984)","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: FOCS, pp. 319\u2013327 (1988)","key":"10_CR20","DOI":"10.1109\/SFCS.1988.21948"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"P.A. Sistla","year":"1994","unstructured":"Sistla, P.A.: Safety, liveness and fairness in temporal logic. Formal Aspects in Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects in Computing"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"P.A. Sistla","year":"1987","unstructured":"Sistla, P.A., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"10_CR23","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":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Tasiran","year":"1995","unstructured":"Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322\u2013331 (1986)","key":"10_CR25"},{"issue":"1\u20132","key":"10_CR26","first-page":"72","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. I&C\u00a056(1\u20132), 72\u201399 (1983)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T14:50:10Z","timestamp":1740840610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}