{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:30:01Z","timestamp":1725564601540},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212362"},{"type":"electronic","value":"9783540247494"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24749-4_46","type":"book-chapter","created":{"date-parts":[[2010,9,8]],"date-time":"2010-09-08T15:01:54Z","timestamp":1283958114000},"page":"522-533","source":"Crossref","is-referenced-by-count":5,"title":["A Measured Collapse of the Modal \u03bc-Calculus Alternation Hierarchy"],"prefix":"10.1007","author":[{"given":"Doron","family":"Bustan","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"46_CR1","volume-title":"Foundations of databases","author":"S. Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of databases. Addison-Wesley, Reading (1995)"},{"key":"46_CR2","unstructured":"van Benthem, J.F.A.K.: Modal Logic and Classical Logic, Bibliopolis, Naples (1985)"},{"key":"46_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Bhat","year":"1996","unstructured":"Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal \u03bc-calculus. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, Springer, Heidelberg (1996)"},{"issue":"2","key":"46_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(97)00217-X","volume":"195","author":"J.C. Bradfield","year":"1998","unstructured":"Bradfield, J.C.: The modal \u03bc-calculus alternation hierarchy is strict. TCS\u00a0195(2), 133\u2013153 (1998)","journal-title":"TCS"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers\u00a0C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"46_CR6","first-page":"142","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. I & C\u00a098(2), 142\u2013170 (1992)","journal-title":"I & C"},{"issue":"2\/3","key":"46_CR7","first-page":"171","volume":"10","author":"R. Bahar","year":"1997","unstructured":"Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. FMSD\u00a010(2\/3), 171\u2013206 (1997)","journal-title":"FMSD"},{"key":"46_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-45657-0_35","volume-title":"Computer Aided Verification","author":"A. Chakrabarti","year":"2002","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzinski, M., Mang, F.Y.C.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 428\u2013441. Springer, Heidelberg (2002)"},{"key":"46_CR9","volume-title":"Perspectives in Mathematical Logic.","author":"H.D. Ebbinghaus","year":"1995","unstructured":"Ebbinghaus, H.D., Flum, J.: Finite Model Theory. In: Perspectives in Mathematical Logic., Springer, Heidelberg (1995)"},{"key":"46_CR10","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1090\/dimacs\/031\/06","volume-title":"Descriptive Complexity and Finite Models","author":"E.A. Emerson","year":"1997","unstructured":"Emerson, E.A.: Modal Checking and the \u03bc-Calculus. In: Descriptive Complexity and Finite Models, pp. 185\u2013214. American Mathematical Society, Providence (1997)"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proc. 7th ICALP, pp. 169\u2013181 (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"46_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C., Sistla, A.P.: On model-checking for fragments of \u03bc-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 385\u2013396. Springer, Heidelberg (1993)"},{"key":"46_CR13","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc. 1st LICS, pp. 267\u2013278 (1986)"},{"key":"46_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","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, R.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, pp. 694\u2013707. Springer, Heidelberg (2001)"},{"key":"46_CR15","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0168-0072(86)90055-2","volume":"32","author":"Y. Gurevich","year":"1986","unstructured":"Gurevich, Y., Shelah, S.: Fixed-point extensions of first-order logic. Annals of Pure and Applied Logic\u00a032, 265\u2013280 (1986)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"46_CR16","first-page":"64","volume":"173","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. I&C\u00a0173(1), 64\u201381 (2002)","journal-title":"I&C"},{"key":"46_CR17","first-page":"86","volume":"68","author":"N. Immerman","year":"1986","unstructured":"Immerman, N.: Relational queries computable in polynomial time. I&C\u00a068, 86\u2013104 (1986)","journal-title":"I&C"},{"key":"46_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/10722167_18","volume-title":"Computer Aided Verification","author":"M. Jurdzinski","year":"2000","unstructured":"Jurdzinski, M., Voge, J.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 202\u2013215. Springer, Heidelberg (2000)"},{"issue":"3","key":"46_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzinski","year":"1998","unstructured":"Jurdzinski, M.: Deciding the winner in parity games is in UP \u2229 co-UP. IPL\u00a068(3), 119\u2013124 (1998)","journal-title":"IPL"},{"key":"46_CR20","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. Jurdzinski","year":"2000","unstructured":"Jurdzinski, 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":"46_CR21","doi-asserted-by":"crossref","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358\u2013367 (1991)","DOI":"10.1109\/SFCS.1991.185391"},{"key":"46_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. TCS\u00a027, 333\u2013354 (1983)","journal-title":"TCS"},{"key":"46_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Proc. 30th STOC, pp. 224\u2013233 (1998)","DOI":"10.1145\/276698.276748"},{"issue":"2","key":"46_CR24","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2001","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM ToCL\u00a02001(2), 408\u2013429 (2001)","journal-title":"ACM ToCL"},{"issue":"2","key":"46_CR25","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"46_CR26","first-page":"95","volume":"89","author":"D. Leivant","year":"1990","unstructured":"Leivant, D.: Inductive definitions over finite structures. I&C\u00a089, 95\u2013108 (1990)","journal-title":"I&C"},{"key":"46_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-58179-0_66","volume-title":"Computer Aided Verification","author":"D. Long","year":"1994","unstructured":"Long, D., Brown, A., Clarke, E., Jha, S., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 338\u2013350. Springer, Heidelberg (1994)"},{"key":"46_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"46_CR29","volume-title":"Elementary Induction on Abstract Structures","author":"Y.N. Moschovakis","year":"1974","unstructured":"Moschovakis, Y.N.: Elementary Induction on Abstract Structures. North-Holland, Amsterdam (1974)"},{"issue":"1","key":"46_CR30","first-page":"151","volume":"107","author":"N. Klarlund","year":"1993","unstructured":"Klarlund, N., Schneider, F.B.: Proving nondeterministically specified safety properties using progress measures. I&C\u00a0107(1), 151\u2013170 (1993)","journal-title":"I&C"},{"key":"46_CR31","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. Park","year":"1976","unstructured":"Park, D.: Finiteness is \u03bc-ineffable. TCS\u00a03, 173\u2013181 (1976)","journal-title":"TCS"},{"key":"46_CR32","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: A decidable \u03bc-calculus: preliminary report. In: 22nd FOCS, pp. 421\u2013427 (1981)","DOI":"10.1109\/SFCS.1981.4"},{"issue":"6","key":"46_CR33","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0020-0190(96)00130-5","volume":"59","author":"H. Seidl","year":"1996","unstructured":"Seidl, H.: Fast and simple nested fixpoints. IPL\u00a059(6), 303\u2013308 (1996)","journal-title":"IPL"}],"container-title":["Lecture Notes in Computer Science","STACS 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24749-4_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,4]],"date-time":"2019-06-04T01:33:39Z","timestamp":1559612019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24749-4_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212362","9783540247494"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24749-4_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}