{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:01Z","timestamp":1760202541770},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_34","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"423-437","source":"Crossref","is-referenced-by-count":30,"title":["The Complexity of the Graded \u03bc-Calculus"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Ulrike","family":"Sattler","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"34_CR1","series-title":"Lect Notes Comput Sci","first-page":"62","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1987","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Temporal Logic in Specification, volume 398 of LNCS, pages 62\u201374. Springer-Verlag, 1987."},{"key":"34_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ofTACAS-96","author":"B. G","year":"1996","unstructured":"G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal \u03bc-calculus. In Proc. ofTACAS-96, LNCS 1055. Springer-Verlag, 1996."},{"key":"34_CR3","first-page":"109","volume":"4","author":"F. Baader","year":"1994","unstructured":"F. Baader, E. Franconi, B. Hollunder, B. Nebel, and H.J. Profitlich. An empirical analysis of optimization techniques for terminological representation systems, or: Making KRIS get a move on. Applied Artificial Intelligence, 4:109\u2013132, 1994.","journal-title":"Applied Artificial Intelligence"},{"issue":"3","key":"34_CR4","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1093\/logcom\/9.3.319","volume":"9","author":"F. Baader","year":"1999","unstructured":"F. Baader and U. Sattler. Expressive number restrictions in description logics. Journal of Logic and Computation, 9(3):319\u2013350, 1999.","journal-title":"Journal of Logic and Computation"},{"key":"34_CR5","unstructured":"D. Calvanese, G. De Giacomo, and M. Lenzerini. Reasoning in expressive description logics with fixpoints based on automata on infinite trees. In IJCAI\u201999, 1999."},{"key":"34_CR6","unstructured":"G. De Giacomo. Decidability of Class-Based Knowledge Representation Formalisms. PhD thesis, Universit\u00e0 degli Studi di Roma \u201cLa Sapienza\u201d, 1995."},{"key":"34_CR7","unstructured":"G. De Giacomo and M. Lenzerini. Boosting the correspondence between description logics and propositional dynamic logics. In Proc. of AAAI-94, 1994."},{"key":"34_CR8","unstructured":"G. De Giacomo and M. Lenzerini. Concept language with number restrictions and fixpoints, and its relationship with mu-calculus. In Proc. of ECAI-94, 1994."},{"key":"34_CR9","unstructured":"F. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. In Proc. of KR-91, 1991."},{"key":"34_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Proc. 4th CAV","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of \u03bc-calculus. In Proc. 4th CAV, LNCS 697, pages 385\u2013396. Springer-Verlag, 1993."},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Model checking and the \u03bc-calculus. In Descriptive Complexity and Finite Models, pages 185\u2013214. American Mathematical Society, 1997.","DOI":"10.1090\/dimacs\/031\/06"},{"key":"34_CR12","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1305\/ndjfl\/1093890715","volume":"13","author":"K. Fine","year":"1972","unstructured":"K. Fine. In so many possible worlds. Notre Dame Journal of Formal Logics, 13:516\u2013520, 1972.","journal-title":"Notre Dame Journal of Formal Logics"},{"key":"34_CR13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"34_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.2307\/421196","volume":"3","author":"E. Gr\u00e4del","year":"1997","unstructured":"E. Gr\u00e4del, Ph. G. Kolaitis, and M. Y. Vardi. The decision problem for 2-variable first-order logic. Bulletin of Symbolic Logic, 3:53\u201369, 1997.","journal-title":"Bulletin of Symbolic Logic"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"E. Gr\u00e4del, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In Proc. of LICS-97, 1997.","DOI":"10.1109\/LICS.1997.614957"},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"E. Gr\u00e4del. On the restraining power of guards. Journal of Symbolic Logic, 64, 1999.","DOI":"10.2307\/2586808"},{"key":"34_CR17","unstructured":"B. Hollunder and F. Baader. Qualifying number restrictions in concept languages. In Proc. of KR-91, pages 335\u2013346, 1991."},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"V Haarslev and R. M\u00f6ller. RACER system description. In Proc. of IJCAR-01, volume 2083 of LNAI. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_59"},{"key":"34_CR19","unstructured":"I. Horrocks. Using an Expressive Description Logic: FaCT or Fiction? In Proc. of KR-98, 1998."},{"key":"34_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CADE-17","author":"I. Horrocks","year":"2000","unstructured":"I. Horrocks, U. Sattler, and S. Tobies. Reasoning with individuals for the description logic shiq. In Proc. of CADE-17, LNCS 1831, Germany, 2000. Springer-Verlag."},{"key":"34_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Proc. of MFCS-95","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal \u03bc-calculus and related results. In Proc. of MFCS-95, LNCS, pages 552\u2013562. Springer-Verlag, 1995."},{"key":"34_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Weak alternating automata and tree automata emptiness. In Proc. STOC-98, pages 224\u2013233, 1998.","DOI":"10.1145\/276698.276748"},{"issue":"2","key":"34_CR24","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, March 2000.","journal-title":"Journal of the ACM"},{"issue":"3","key":"34_CR25","first-page":"467","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Control and Optimization, 6(3):467\u2013480, 1977.","journal-title":"SIAM Journal of Control and Optimization"},{"key":"34_CR26","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/322033.322037","volume":"24","author":"N. Lynch","year":"1977","unstructured":"N. Lynch. Log space recognition and translation of parenthesis languages. Journal of the ACM, 24:583\u2013590, 1977.","journal-title":"Journal of the ACM"},{"key":"34_CR27","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"key":"34_CR28","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeter-ministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69\u2013107, 1995.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"34_CR29","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/122296.122313","volume":"2","author":"P.-S. P","year":"1991","unstructured":"P. Patel-Schneider, D. McGuinness, R. Brachman, L. Resnick, and A. Borgida. The CLASSIC knowledge representation system: Guiding principles and implementation rationale. SIGART Bulletin, 2(3): 108\u2013113, 1991.","journal-title":"SIGART Bulletin"},{"issue":"4","key":"34_CR30","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"L. Pacholski, W. Szwast, and L. Tendera. Complexity results for first-order two-variable logic with counting. SIAM Journal of Computing, 29(4): 1083\u20131117, 2000.","journal-title":"SIAM Journal of Computing"},{"key":"34_CR31","series-title":"PhD thesis","volume-title":"Complexity of automata on infinite objects","author":"S. Safra","year":"1989","unstructured":"S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1989."},{"key":"34_CR32","doi-asserted-by":"crossref","unstructured":"K. Schild. Terminological cycles and the propositional \u03bc-calculus. In Proc. of KR-94, pages 509\u2013520. Morgan Kaufmann, 1994.","DOI":"10.1016\/B978-1-4832-1452-8.50142-1"},{"issue":"3","key":"34_CR33","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"R.S. Streett","year":"1989","unstructured":"R.S. Streett and E.A. Emerson. An automata theoretic decision procedure for the propositional \u03bc-calculus. Information and Computation, 81(3):249\u2013264, 1989.","journal-title":"Information and Computation"},{"key":"34_CR34","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 165\u2013191. North Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"34_CR35","doi-asserted-by":"crossref","unstructured":"W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Language Theory, volume III, pages 389\u2013455, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"34_CR36","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1613\/jair.705","volume":"12","author":"S. Tobies","year":"2000","unstructured":"S. Tobies. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. Journal of Artificial Intelligence Research, 12:199\u2013217, 2000.","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"1","key":"34_CR37","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1093\/logcom\/11.1.85","volume":"11","author":"S. Tobies","year":"2001","unstructured":"S. Tobies. PSPACE reasoning for graded modal logics. Journal of Logic and Computation, 11(1):85\u2013106, 2001.","journal-title":"Journal of Logic and Computation"},{"key":"34_CR38","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. What makes modal logic so robustly decidable? In Descriptive Complexity and Finite Models, pages 149\u2013183. American Mathematical Society, 1997.","DOI":"10.1090\/dimacs\/031\/05"},{"issue":"3","key":"34_CR39","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1093\/logcom\/5.3.325","volume":"5","author":"W. Hoek van der","year":"1995","unstructured":"W van der Hoek and M. De Rijke. Counting objects. Journal of Logic and Computation, 5(3):325\u2013345, 1995.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"34_CR40","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2): 182\u2013221, 1986.","journal-title":"Journal of Computer and System Science"},{"key":"34_CR41","series-title":"Lect Notes Comput Sci","first-page":"401","volume-title":"Proc. of STACS-96","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Monadic second order logic on tree-like structures. In Proc. of STACS-96, LNCS, pages 401\u2013413. Springer-Verlag, 1996."},{"key":"34_CR42","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Proc. of FSTTCS-99","author":"T. Wilke","year":"1999","unstructured":"T. Wilke. CTL+ is exponentially more succinct than CTL. In Proc. of FSTTCS-99, volume 1738 of LNCS, pages 110\u2013121. Springer-Verlag, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:55:45Z","timestamp":1556754945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_34","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}