Voir la notice de l'article provenant de la source Numdam
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).
@article{ITA_2013__47_1_97_0,
author = {Parys, Pawe{\l}},
title = {Some results on complexity of $\mu $-calculus evaluation in the black-box model},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {97--109},
publisher = {EDP-Sciences},
volume = {47},
number = {1},
year = {2013},
doi = {10.1051/ita/2012030},
zbl = {1269.68056},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2012030/}
}
TY - JOUR AU - Parys, Paweł TI - Some results on complexity of $\mu $-calculus evaluation in the black-box model JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2013 SP - 97 EP - 109 VL - 47 IS - 1 PB - EDP-Sciences UR - http://geodesic.mathdoc.fr/articles/10.1051/ita/2012030/ DO - 10.1051/ita/2012030 LA - en ID - ITA_2013__47_1_97_0 ER -
%0 Journal Article %A Parys, Paweł %T Some results on complexity of $\mu $-calculus evaluation in the black-box model %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2013 %P 97-109 %V 47 %N 1 %I EDP-Sciences %U http://geodesic.mathdoc.fr/articles/10.1051/ita/2012030/ %R 10.1051/ita/2012030 %G en %F ITA_2013__47_1_97_0
Parys, Paweł. Some results on complexity of $\mu $-calculus evaluation in the black-box model. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 1, pp. 97-109. doi: 10.1051/ita/2012030
Cité par Sources :