Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity in time and linear program complexity in space for and alternation-free modal -calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for (modal -calculus with fixed alternation-depth at most ).
Mots-clés : databases, model-checking, specification languages, performance evaluation
@article{ITA_2009__43_1_1_0, author = {Foustoucos, Eug\'enie and Guessarian, Ir\`ene}, title = {Inf-datalog, modal logic and complexities}, journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications}, pages = {1--21}, publisher = {EDP-Sciences}, volume = {43}, number = {1}, year = {2009}, doi = {10.1051/ita:2007043}, mrnumber = {2483442}, zbl = {1170.68015}, language = {en}, url = {http://archive.numdam.org/articles/10.1051/ita:2007043/} }
TY - JOUR AU - Foustoucos, Eugénie AU - Guessarian, Irène TI - Inf-datalog, modal logic and complexities JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2009 SP - 1 EP - 21 VL - 43 IS - 1 PB - EDP-Sciences UR - http://archive.numdam.org/articles/10.1051/ita:2007043/ DO - 10.1051/ita:2007043 LA - en ID - ITA_2009__43_1_1_0 ER -
%0 Journal Article %A Foustoucos, Eugénie %A Guessarian, Irène %T Inf-datalog, modal logic and complexities %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2009 %P 1-21 %V 43 %N 1 %I EDP-Sciences %U http://archive.numdam.org/articles/10.1051/ita:2007043/ %R 10.1051/ita:2007043 %G en %F ITA_2009__43_1_1_0
Foustoucos, Eugénie; Guessarian, Irène. Inf-datalog, modal logic and complexities. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 1, pp. 1-21. doi : 10.1051/ita:2007043. http://archive.numdam.org/articles/10.1051/ita:2007043/
[1] Foundations of databases. Addison-Wesley (1995). | Zbl
, and ,[2] A linear algorithm to solve fixed-point equations on transition systems. Inform. Process. Lett. 29 (1988) 57-66. | MR | Zbl
and ,[3] Rudiments of -calculus. Stud. Logic Found. Math. 146, Elsevier Science, North-Holland, Amsterdam (2001). | MR | Zbl
and ,[4] Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO-Theor. Inf. Appl. 33 (1999) 341-356. | Numdam | MR | Zbl
,[5] An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci. 178 (1997) 237-255. | MR | Zbl
, , , and ,[6] The horn Mu-calculus. LICS (1998) 58-69. | MR | Zbl
, , , and ,[7] Automatic Verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8 (1986) 244-263. | Zbl
, and ,[8] A linear time model-checking algorithm for the alternation-free modal mu-calculus. Formal Method. Syst. Des. 2 (1993) 121-148. | Zbl
and ,[9] Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997-1072. | MR | Zbl
,[10] Model-Checking and the Mu-Calculus, in Descriptive Complexity and Finite Models, edited by N. Immerman and Ph. Kolaitis, American Mathematical Society (1997). | MR | Zbl
,[11] Efficient model-checking in fragments of the propositional -calculus, in Proc. of 1rst Symposium on Logic in Computer Science (1986) 267-278.
and ,[12] Complexity of Monadic inf-datalog. Application to temporal logic. Extended abstract in Proceedings 4th Panhellenic Logic Symposium (2003) 95-99.
and ,[13] Monadic Datalog and the expressive power of web information extraction languages. Proc. PODS'02 (2002) 17-28.
and ,[14] Datalog LITE: temporal versus deductive reasoning in verification. ACM T. Comput. Log. 3 (2002) 39-74. | MR
, and ,[15] The Mec 5 model-checker, CAV'04. Lect. Notes Comput. Sci. 3114 (2004) 488-491. | Zbl
and ,[16] On temporal logic versus Datalog. Theor. Comput. Sci. 303 (2003) 103-133. | MR | Zbl
, , and ,[17] Small progress measures for solving parity games. Proc. STACS'2000 (2000) 290-301. | MR | Zbl
,[18] A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117-123. | MR
, and ,[19] Results on the propositional -calculus. Theor. Comput. Sci. 27 (1983) 333-354. | MR | Zbl
,[20] The modal -calculus, model-checking, equations systems and Gauss elimination. TACAS 95 (1995) 44-57.
,[21] Finiteness is -ineffable. Theor. Comput. Sci. 3 (1976) 173-181. | MR | Zbl
,[22] Fast and simple nested fixpoints. Inform. Process. Lett. 59 (1996) 303-308. | MR | Zbl
,[23] Conception et réalisation d'un vérificateur de modèles AltaRica. Ph.D. Thesis, LaBRI, University of Bordeaux 1 (2003) http://altarica.labri.fr/Doc/Biblio/Author/VINCENT-A.html
,Cité par Sources :