{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:19:36Z","timestamp":1759637976473,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319270593"},{"type":"electronic","value":"9783319270609"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-27060-9_14","type":"book-chapter","created":{"date-parts":[[2015,11,19]],"date-time":"2015-11-19T15:14:30Z","timestamp":1447946070000},"page":"178-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Model Checking of the Graded $$\\mu $$ -calculus on Trees"],"prefix":"10.1007","author":[{"given":"Everardo","family":"B\u00e1rcenas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edgard","family":"Ben\u00edtez-Guerrero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Lavalle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,30]]},"reference":[{"key":"14_CR1","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, pp. 306\u2013317. IEEE Computer Society (1997)"},{"key":"14_CR2","unstructured":"Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335\u2013346. Morgan Kaufmann (1991)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-45620-1_34","volume-title":"Automated Deduction - CADE-18","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded $$\\mu $$ -calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423\u2013437. Springer, Heidelberg (2002)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched mu-calculi. Logical Methods in Computer Science 4(3) (2008)","DOI":"10.2168\/LMCS-4(3:11)2008"},{"key":"14_CR5","unstructured":"B\u00e1rcenas, E., Genev\u00e8s, P., Laya\u00efda, N., Schmitt, A.: Query reasoning on trees with types, interleaving, and counting. In: Walsh, T. (ed.) IJCAI. IJCAI\/AAAI (2011)"},{"issue":"2","key":"14_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^20$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"14_CR7","volume-title":"Model Checking","author":"EM Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"2","key":"14_CR8","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343\u2013352 (2009)","journal-title":"Automatica"},{"issue":"1\u20132","key":"14_CR9","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/S0304-3975(00)00034-7","volume":"258","author":"EA Emerson","year":"2001","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the $${\\mu }$$ -calculus and its fragments. Theor. Comput. Sci. 258(1\u20132), 491\u2013522 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods Syst. Des. 2(2), 121\u2013147 (1993)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Giacomo, G.D., Lenzerini, M., Vardi, M.Y.: Node selection query languages for trees. In: Fox, M., Poole, D. (eds.) AAAI. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7598"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Ferrante, A., Murano, A., Parente, M.: Enriched $${\\mu }$$ -calculi module checking. Logical Methods in Computer Science 4(3) (2008)","DOI":"10.2168\/LMCS-4(3:1)2008"},{"key":"14_CR13","unstructured":"Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata. Texts in Logic and Games, vol. 2, pp. 575\u2013612. Amsterdam University Press (2008)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.jal.2010.03.001","volume":"8","author":"S Demri","year":"2010","unstructured":"Demri, S., Lugiez, D.: Complexity of modal logics with Presburger constraints. J. Applied Logic 8(3), 233\u2013252 (2010)","journal-title":"J. Applied Logic"},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/2287718.2287725","volume":"13","author":"A Bianco","year":"2012","unstructured":"Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. ACM Trans. Comput. Log. 13(3), 25 (2012)","journal-title":"ACM Trans. Comput. Log."},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-45114-0_7","volume-title":"Advances in Artificial Intelligence and Its Applications","author":"E B\u00e1rcenas","year":"2013","unstructured":"B\u00e1rcenas, E., Lavalle, J.: Expressive reasoning on tree structures: recursion, inverse programs, Presburger constraints and nominals. In: Castro, F., Gelbukh, A., Gonz\u00e1lez, M. (eds.) MICAI 2013, Part I. LNCS, vol. 8265, pp. 80\u201391. Springer, Heidelberg (2013)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"B\u00e1rcenas, E., Lavalle, J.: Global numerical constraints on trees. Logical Methods in Computer Science 10(2) (2014)","DOI":"10.2168\/LMCS-10(2:10)2014"},{"issue":"1","key":"14_CR18","first-page":"1","volume":"9","author":"F Laroussinie","year":"2012","unstructured":"Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. Logical Methods Comput. Sci. 9(1), 1\u201334 (2012)","journal-title":"Logical Methods Comput. Sci."},{"issue":"3","key":"14_CR19","doi-asserted-by":"crossref","first-page":"323","DOI":"10.3233\/FI-2009-181","volume":"96","author":"A Ferrante","year":"2009","unstructured":"Ferrante, A., Napoli, M., Parente, M.: Model checking for graded CTL. Fundam. Inform. 96(3), 323\u2013339 (2009)","journal-title":"Fundam. Inform."},{"issue":"2","key":"14_CR20","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2724712","volume":"16","author":"P Genev\u00e8s","year":"2015","unstructured":"Genev\u00e8s, P., Laya\u00efda, N., Schmitt, A., Gesbert, N.: Efficiently deciding $$\\mu $$ -calculus with converse over finite trees. ACM Trans. Comput. Logic 16(2), 16:1\u201316:41 (2015)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"2","key":"14_CR21","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/1059513.1059520","volume":"52","author":"G Gottlob","year":"2005","unstructured":"Gottlob, G., Koch, C., Pichler, R., Segoufin, L.: The complexity of XPath query evaluation and XML typing. J. ACM 52(2), 284\u2013335 (2005)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence and Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27060-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T22:31:45Z","timestamp":1692138705000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27060-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319270593","9783319270609"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27060-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"30 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}