We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Some results on complexity of μ-calculus evaluation in the black-box model.
- Authors
Parys, Paweł
- Abstract
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).
- Subjects
COMPUTATIONAL complexity; CALCULUS; MATHEMATICAL formulas; PROBLEM solving; MONOTONE operators; COMPUTER algorithms
- Publication
RAIRO - Theoretical Informatics & Applications, 2013, Vol 47, Issue 1, p97
- ISSN
2804-7346
- Publication type
Article
- DOI
10.1051/ita/2012030