Some results on complexity of μ-calculus evaluation in the black-box model

Paweł Parys

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2013)

  • Volume: 47, Issue: 1, page 97-109
  • ISSN: 0988-3754

Abstract

top
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).

How to cite

top

Parys, Paweł. "Some results on complexity of μ-calculus evaluation in the black-box model." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 47.1 (2013): 97-109. <http://eudml.org/doc/273068>.

@article{Parys2013,
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).},
author = {Parys, Paweł},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {μ-calculus; black-box model; lower bound; expression complexity; -calculus},
language = {eng},
number = {1},
pages = {97-109},
publisher = {EDP-Sciences},
title = {Some results on complexity of μ-calculus evaluation in the black-box model},
url = {http://eudml.org/doc/273068},
volume = {47},
year = {2013},
}

TY - JOUR
AU - Parys, Paweł
TI - Some results on complexity of μ-calculus evaluation in the black-box model
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2013
PB - EDP-Sciences
VL - 47
IS - 1
SP - 97
EP - 109
AB - 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).
LA - eng
KW - μ-calculus; black-box model; lower bound; expression complexity; -calculus
UR - http://eudml.org/doc/273068
ER -

References

top
  1. [1] A. Arnold and D. Niwiński, Rudiments of μ-Calculus, Studies in Logic and the Foundations of Mathematics. North Holland 146 (2001). Zbl0968.03002
  2. [2] A. Dawar and S. Kreutzer, Generalising automaticity to modal properties of finite structures. Theor. Comput. Sci.379 (2007) 266–285. Zbl1121.03046
  3. [3] S. Dziembowski, M. Jurdziński and D. Niwiński, On the expression complexity of the modal μ-calculus model checking, unpublished manuscript. 
  4. [4] E.A. Emerson and C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus (extended abstract), in Proc. of 1st Ann. IEEE Symp. on Logic in Computer Science, LICS ’86 Cambridge, MA, June 1986. IEEE CS Press. (1986) 267–278. 
  5. [5] M. Jurdziński, M. Paterson and U. Zwick, A deterministic subexponential algorithm for solving parity games. SIAM J. Comput.38 (2008) 1519–1532. Zbl1173.91326
  6. [6] D.E. Long, A. Browne, E.M. Clarke, S. Jha and W.R. Marrero, An improved algorithm for the evaluation of fixpoint expressions. in Proc. of 6th Int. Conf. on Computer Aided Verification, CAV ’94 Stanford, CA, June 1994, edited by D. L. Dill, Springer, Lect. Notes Comput. Sci. 818 (1994) 338–350. Zbl0901.68118
  7. [7] D. Niwiński, Computing flat vectorial Boolean fixed points, unpublished manuscript. 
  8. [8] S. Schewe, Solving parity games in big steps, in Proc. of 27th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2007 Kharagpur, Dec. 2007, edited by V. Arvind and S. Prasad, Springer. Lect. Notes Comput. Sci. 4855 (2007) 449–460. Zbl1135.68480MR2480222
  9. [9] S. Zhang, O. Sokolsky and S.A. Smolka, On the parallel complexity of model checking in the modal mu-calculus, in Proc. 9th Ann. IEEE Symp. on Logic in Computer Science, LICS ’94 Paris, July 1994. IEEE CS Press. (1994) 154–163. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.