RAIRO-Theor. Inf. Appl.
Volume 47, Number 1, January-March 2013
6th Workshop on Fixed Points in Computer Science (FICS'09)
|Page(s)||97 - 109|
|Published online||10 January 2013|
Some results on complexity of μ-calculus evaluation in the black-box model∗
Institute of Informatics, University of Warsaw,
ul. Banacha 2, 02-097
Accepted: 28 September 2012
We consider μ-calculus formulas in a normal form: after a prefix of fixed-point quantifiers follows a quantifier-free expression. We are interested in the problem of evaluating (model checking) such formulas in a powerset lattice. We assume that the quantifier-free part of the expression can be any monotone function given by a black-box – we may only ask for its value for given arguments. As a first result we prove that when the lattice is fixed, the problem becomes polynomial (the assumption about the quantifier-free part strengthens this result). As a second result we show that any algorithm solving the problem has to ask at least about n2 (namely Ω(n2/log n)) queries to the function, even when the expression consists of one μ and one ν (the assumption about the quantifier-free part weakens this result).
Mathematics Subject Classification: 68Q17 / 03B70
Key words: μ-calculus / black-box model / lower bound / expression complexity
© EDP Sciences 2013
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.