{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:19:50Z","timestamp":1725560390748},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540287025"},{"type":"electronic","value":"9783540318675"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11549345_55","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:05:47Z","timestamp":1127829947000},"page":"640-651","source":"Crossref","is-referenced-by-count":2,"title":["The Complexity of Model Checking Higher Order Fixpoint Logic"],"prefix":"10.1007","author":[{"given":"Martin","family":"Lange","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafa\u0142","family":"Somla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"55_CR1","first-page":"113","volume":"14","author":"Y. Bar-Hillel","year":"1961","unstructured":"Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Zeitschrift f\u00fcr Phonologie, Sprachwissenschaft und Kommunikationsforschung\u00a014, 113\u2013124 (1961)","journal-title":"Zeitschrift f\u00fcr Phonologie, Sprachwissenschaft und Kommunikationsforschung"},{"issue":"8","key":"55_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"55_CR3","first-page":"1","volume-title":"Proc. Congress on Logic, Method, and Philosophy of Science","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Congress on Logic, Method, and Philosophy of Science, Stanford, CA, USA, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"issue":"2","key":"55_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","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. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"issue":"1","key":"55_CR5","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"Journal of the ACM"},{"issue":"1","key":"55_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"55_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-44802-0_20","volume-title":"Computer Science Logic","author":"A. Dawar","year":"2001","unstructured":"Dawar, A., Gr\u00e4del, E., Kreutzer, S.: Inflationary fixed points in modal logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 277\u2013291. Springer, Heidelberg (2001)"},{"issue":"2","key":"55_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0020-0190(87)90097-4","volume":"24","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A.: Uniform inevitability is tree automaton ineffable. Information Processing Letters\u00a024(2), 77\u201379 (1987)","journal-title":"Information Processing Letters"},{"key":"55_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences\u00a030, 1\u201324 (1985)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"55_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"55_CR11","first-page":"368","volume-title":"Proc. 32nd Symp. on Foundations of Computer Science","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, \u03bc-calculus and determinacy. In: Proc. 32nd Symp. on Foundations of Computer Science, San Juan, Puerto Rico, oct 1991, pp. 368\u2013377. IEEE Computer Society Press, Los Alamitos (1991)"},{"issue":"2","key":"55_CR12","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences\u00a018(2), 194\u2013211 (1979)","journal-title":"Journal of Computer and System Sciences"},{"issue":"2","key":"55_CR13","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1016\/0022-0000(83)90014-4","volume":"26","author":"D. Harel","year":"1983","unstructured":"Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences\u00a026(2), 222\u2013243 (1983)","journal-title":"Journal of Computer and System Sciences"},{"key":"55_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., Joergensen, M., Klarlund, N.: MONA: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 89\u2013110. Springer, Heidelberg (1995)"},{"key":"55_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"CONCUR 1996: Concurrency Theory","author":"D. Janin","year":"1996","unstructured":"Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional \u03bc-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 263\u2013277. Springer, Heidelberg (1996)"},{"key":"55_CR16","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":"55_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45931-6_18","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Lange","year":"2002","unstructured":"Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 250\u2013263. Springer, Heidelberg (2002)"},{"key":"55_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/3-540-49116-3_48","volume-title":"STACS 1999","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M\u00fcller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.\u00a01563, pp. 510\u2013520. Springer, Heidelberg (1999)"},{"key":"55_CR19","first-page":"46","volume-title":"Proc. 18th Symp. on Foundations of Computer Science, FOCS 1977","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Symp. on Foundations of Computer Science, FOCS 1977, Providence, RI, USA, oct 1977, pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"55_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-36387-4_13","volume-title":"Automata, Logics, and Infinite Games","author":"K. Reinhardt","year":"2002","unstructured":"Reinhardt, K.: 13 the complexity of translating logic to finite automata. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 231\u2013238. Springer, Heidelberg (2002)"},{"key":"55_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R.: The typed \u03bb-calculus is not elementary recursive. Theoretical Computer Science\u00a09, 73\u201381 (1979)","journal-title":"Theoretical Computer Science"},{"key":"55_CR22","unstructured":"Stockmeyer, L.: The Computational Complexity of Word Problems. PhD thesis, MIT (1974)"},{"key":"55_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-28644-8_33","volume-title":"CONCUR 2004 - Concurrency Theory","author":"M. Viswanathan","year":"2004","unstructured":"Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 512\u2013528. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2005"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11549345_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:58:32Z","timestamp":1619506712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11549345_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540287025","9783540318675"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11549345_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}