{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:39Z","timestamp":1751660499288},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-89439-1_16","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"214-229","source":"Crossref","is-referenced-by-count":12,"title":["Alternation Elimination by Complementation (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Christian","family":"Dax","sequence":"first","affiliation":[]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"IEEE standard for property specification language (PSL). IEEE Std. 1850TM (October 2005)","key":"16_CR1"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51803-7_22","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1989","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398. Springer, Heidelberg (1989)"},{"doi-asserted-by":"crossref","unstructured":"Bloem, R., Cimatti, A., Pill, I., Roveri, M.: Symbolic implementation of alternating automata. Int. J. Found. Comput. Sci.\u00a018 (2007)","key":"16_CR3","DOI":"10.1142\/S0129054107004942"},{"doi-asserted-by":"crossref","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log.\u00a06 (2005)","key":"16_CR4","DOI":"10.1145\/1071596.1071601"},{"unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL, tech. report, Computer Science and Applied Mathematics, The Weizmann Institute of Science, Israel (2005)","key":"16_CR5"},{"doi-asserted-by":"crossref","unstructured":"Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. In: Logic and Algebra of Specifications. NATO ASI Series (1993)","key":"16_CR6","DOI":"10.1007\/978-3-642-58041-3_5"},{"doi-asserted-by":"crossref","unstructured":"Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \u03bc-calculus. In: Proc. of FSTTCS 2006. LNCS, vol.\u00a04437 (2006)","key":"16_CR7","DOI":"10.1007\/11944836_26"},{"unstructured":"Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy (extended abstract). In: Proc. of FOCS 1991 (1991)","key":"16_CR8"},{"doi-asserted-by":"crossref","unstructured":"Etessami, K., Wilke, T., Schuller, R.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput.\u00a034 (2005)","key":"16_CR9","DOI":"10.1137\/S0097539703420675"},{"doi-asserted-by":"crossref","unstructured":"Fritz, C., Wilke, T.: Simulation relations for alternating B\u00fcchi automata. Theoret. Comput. Sci.\u00a0338 (2005)","key":"16_CR10","DOI":"10.1016\/j.tcs.2005.01.016"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","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, p. 53. Springer, Heidelberg (2001)"},{"key":"16_CR12","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)"},{"doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of PSTV 1995. IFIP Conf. Proc., vol.\u00a038 (1996)","key":"16_CR13","DOI":"10.1007\/978-0-387-34892-6_1"},{"doi-asserted-by":"crossref","unstructured":"Jutla, C.: Determinization and memoryless winning strategies. Inf. Comput.\u00a0133 (1997)","key":"16_CR14","DOI":"10.1006\/inco.1997.2624"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/3-540-44685-0_35","volume-title":"CONCUR 2001 - Concurrency Theory","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Piterman, N., Vardi, M.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, p. 519. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata and tree automata emptiness. In: Proc. of STOC 1998 (1998)","key":"16_CR16","DOI":"10.1145\/276698.276748"},{"doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2 (2001)","key":"16_CR17","DOI":"10.1145\/377978.377993"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-31980-1_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 206\u2013221. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Lange, M., Stirling, C.: Focus games for satisfiability and completeness of temporal logic. In: Proc. of LICS 2001 (2001)","key":"16_CR19","DOI":"10.1109\/LICS.2001.932511"},{"unstructured":"L\u00f6ding, C.: Methods for the transformation of omega-automata: Complexity and connection to second order logic, master\u2019s thesis, University of Kiel, Germany (1998)","key":"16_CR20"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoret. Comput. Sci.\u00a032 (1984)","key":"16_CR22","DOI":"10.1016\/0304-3975(84)90049-5"},{"doi-asserted-by":"crossref","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of trees and its complexity. Theoret. Comput. Sci.\u00a097 (1992)","key":"16_CR23","DOI":"10.1016\/0304-3975(92)90076-R"},{"doi-asserted-by":"crossref","unstructured":"Muller, D., Schupp, P.: Alternating automata on infinite trees. Theoret. Comput. Sci.\u00a054 (1987)","key":"16_CR24","DOI":"10.1016\/0304-3975(87)90133-2"},{"doi-asserted-by":"crossref","unstructured":"Muller, D., Schupp, P.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoret. Comput. Sci.\u00a0141 (1995)","key":"16_CR25","DOI":"10.1016\/0304-3975(94)00214-4"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS 1977 (1977)","key":"16_CR26","DOI":"10.1109\/SFCS.1977.32"},{"unstructured":"Rohde, G.: Alternating automata and the temporal logic of ordinals, PhD thesis, University of Illinois at Urbana-Champaign, Champaign, IL, USA (1997)","key":"16_CR27"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M.: A temporal fixpoint calculus. In: Proc. of POPL 1988 (1988)","key":"16_CR28","DOI":"10.1145\/73560.73582"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M.: A note on the reduction of two-way automata to one-way automata. Inform. Process. Lett. 30 (1989)","key":"16_CR29","DOI":"10.1016\/0020-0190(89)90205-6"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"M. Vardi","year":"1998","unstructured":"Vardi, M.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443. Springer, Heidelberg (1998)"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Vardi","year":"2007","unstructured":"Vardi, M.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T13:12:13Z","timestamp":1557925933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}