{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,14]],"date-time":"2026-06-14T09:43:58Z","timestamp":1781430238876,"version":"3.54.1"},"reference-count":9,"publisher":"EDP Sciences","issue":"1","license":[{"start":{"date-parts":[[2013,1,10]],"date-time":"2013-01-10T00:00:00Z","timestamp":1357776000000},"content-version":"vor","delay-in-days":9,"URL":"https:\/\/www.edpsciences.org\/en\/authors\/copyright-and-licensing"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"accepted":{"date-parts":[[2012,9,28]]},"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>We consider <jats:italic>\u03bc<\/jats:italic>-calculus formulas in a normal form: after a prefix of\n          fixed-point quantifiers follows a quantifier-free expression. We are interested in the\n          problem of evaluating (model checking) such formulas in a powerset lattice. We assume that\n          the quantifier-free part of the expression can be any monotone function given by a\n          black-box \u2013 we may only ask for its value for given arguments. As a first result we prove\n          that when the lattice is fixed, the problem becomes polynomial (the assumption about the\n          quantifier-free part strengthens this result). As a second result we show that any\n          algorithm solving the problem has to ask at least about <jats:italic>n<\/jats:italic><jats:sup>2<\/jats:sup>\n          (namely \u03a9(<jats:italic>n<\/jats:italic><jats:sup>2<\/jats:sup>\/log <jats:italic>n<\/jats:italic>)) queries to the function, even when the expression\n          consists of one <jats:italic>\u03bc<\/jats:italic> and one <jats:italic>\u03bd<\/jats:italic> (the assumption about the\n          quantifier-free part weakens this result).<\/jats:p>","DOI":"10.1051\/ita\/2012030","type":"journal-article","created":{"date-parts":[[2013,1,10]],"date-time":"2013-01-10T13:38:17Z","timestamp":1357825097000},"page":"97-109","source":"Crossref","is-referenced-by-count":1,"title":["Some results on complexity of <i>\u03bc<\/i>-calculus\n          evaluation in the black-box model"],"prefix":"10.1051","volume":"47","author":[{"given":"Pawe\u0142","family":"Parys","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"250","published-online":{"date-parts":[[2013,1,10]]},"reference":[{"key":"R1","unstructured":"Arnold A. and Niwi\u0144ski D., Rudiments of\n              \u03bc-Calculus, Studies in Logic and the Foundations of\n              Mathematics. North Holland\n          146 (2001)."},{"key":"R2","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1016\/j.tcs.2007.03.048","volume":"379","author":"Dawar","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"R3","unstructured":"S. Dziembowski, M. Jurdzi\u0144ski and D. Niwi\u0144ski, On\n          the expression complexity of the modal \u03bc-calculus model checking,\n          unpublished manuscript."},{"key":"R4","unstructured":"E.A. Emerson and C.-L. Lei, Efficient model\n          checking in fragments of the propositional mu-calculus (extended abstract), in\n            Proc. of 1st Ann. IEEE Symp. on Logic in Computer Science, LICS \u201986 Cambridge,\n            MA, June 1986. IEEE CS Press. (1986) 267\u2013278."},{"key":"R5","doi-asserted-by":"crossref","first-page":"1519","DOI":"10.1137\/070686652","volume":"38","author":"Jurdzi\u0144ski","year":"2008","journal-title":"SIAM J. Comput."},{"key":"R6","doi-asserted-by":"crossref","unstructured":"D.E. Long, A. Browne, E.M. Clarke, S. Jha and W.R.\n          Marrero, An improved algorithm for the evaluation of fixpoint expressions. in\n            Proc. of 6th Int. Conf. on Computer Aided Verification, CAV \u201994 Stanford, CA,\n            June 1994, edited by D. L. Dill, Springer, Lect. Notes Comput.\n            Sci.\n          818 (1994) 338\u2013350.","DOI":"10.1007\/3-540-58179-0_66"},{"key":"R7","unstructured":"D. Niwi\u0144ski, Computing flat vectorial Boolean\n          fixed points, unpublished manuscript."},{"key":"R8","doi-asserted-by":"crossref","unstructured":"S. Schewe, Solving parity games in big steps, in\n            Proc. of 27th Int. Conf. on Foundations of Software Technology and Theoretical\n            Computer Science, FSTTCS 2007 Kharagpur, Dec. 2007, edited by V. Arvind and S.\n          Prasad, Springer. Lect. Notes Comput. Sci.\n          4855 (2007) 449\u2013460.","DOI":"10.1007\/978-3-540-77050-3_37"},{"key":"R9","unstructured":"S. Zhang, O. Sokolsky and S.A. Smolka, On the\n          parallel complexity of model checking in the modal mu-calculus, in Proc. 9th Ann.\n            IEEE Symp. on Logic in Computer Science, LICS \u201994 Paris, July 1994. IEEE CS\n          Press. (1994) 154\u2013163."}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012030\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,3]],"date-time":"2021-09-03T11:57:08Z","timestamp":1630670228000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012030"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":9,"journal-issue":{"issue":"1"},"alternative-id":["ita120044"],"URL":"https:\/\/doi.org\/10.1051\/ita\/2012030","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"value":"0988-3754","type":"print"},{"value":"1290-385X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}