Inf-datalog, modal logic and complexities

Foustoucos, Eugénie; Guessarian, Irène

doi:10.1051/ita:2007043

Foustoucos, Eugénie ; Guessarian, Irène

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 1, pp. 1-21

Résumé

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 $C T L$ and alternation-free modal $μ$ -calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for $L μ_{k}$ (modal $μ$ -calculus with fixed alternation-depth at most $k$ ).

MR Zbl

DOI : 10.1051/ita:2007043

Classification : 68Q19, 03C13
Keywords: 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},
     year = {2009},
     publisher = {EDP Sciences},
     volume = {43},
     number = {1},
     doi = {10.1051/ita:2007043},
     mrnumber = {2483442},
     zbl = {1170.68015},
     language = {en},
     url = {https://www.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  - https://www.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 https://www.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

Bibliographie
Cité par

[1] S. Abiteboul, R. Hull and V. Vianu, Foundations of databases. Addison-Wesley (1995). | Zbl

[2] A. Arnold and P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems. Inform. Process. Lett. 29 (1988) 57-66. | Zbl | MR

[3] A. Arnold and D. Niwiński, Rudiments of $μ$ -calculus. Stud. Logic Found. Math. 146, Elsevier Science, North-Holland, Amsterdam (2001). | Zbl | MR

[4] J. Bradfield, Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO-Theor. Inf. Appl. 33 (1999) 341-356. | Zbl | MR | Numdam

[5] A. Browne, E. Clarke, S. Jha, D. Long and W. Marrero, An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci. 178 (1997) 237-255. | Zbl | MR

[6] W. Charatonik, D. Mcallester, D. Niwínski, A. Podelski and I. Walukiewicz, The horn Mu-calculus. LICS (1998) 58-69. | Zbl | MR

[7] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic Verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8 (1986) 244-263. | Zbl

[8] R. Cleaveland and B. Steffan, A linear time model-checking algorithm for the alternation-free modal mu-calculus. Formal Method. Syst. Des. 2 (1993) 121-148. | Zbl

[9] E. Emerson, Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997-1072. | Zbl | MR

[10] E. Emerson, Model-Checking and the Mu-Calculus, in Descriptive Complexity and Finite Models, edited by N. Immerman and Ph. Kolaitis, American Mathematical Society (1997). | Zbl | MR

[11] E.A. Emerson and C.L. Lei, Efficient model-checking in fragments of the propositional $μ$ -calculus, in Proc. of 1rst Symposium on Logic in Computer Science (1986) 267-278.

[12] E. Foustoucos and I. Guessarian, Complexity of Monadic inf-datalog. Application to temporal logic. Extended abstract in Proceedings 4th Panhellenic Logic Symposium (2003) 95-99.

[13] G. Gottlob and C. Koch, Monadic Datalog and the expressive power of web information extraction languages. Proc. PODS'02 (2002) 17-28.

[14] G. Gottlob, E. Grädel and H. Veith, Datalog LITE: temporal versus deductive reasoning in verification. ACM T. Comput. Log. 3 (2002) 39-74. | MR

[15] A. Griffault and A. Vincent, The Mec 5 model-checker, CAV'04. Lect. Notes Comput. Sci. 3114 (2004) 488-491. | Zbl

[16] I. Guessarian, E. Foustoucos, T. Andronikos and F. Afrati, On temporal logic versus Datalog. Theor. Comput. Sci. 303 (2003) 103-133. | Zbl | MR

[17] M. Jurdzinski, Small progress measures for solving parity games. Proc. STACS'2000 (2000) 290-301. | Zbl | MR

[18] M. Jurdzinski, M. Paterson and U. Zwick, A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117-123. | MR

[19] D. Kozen, Results on the propositional $μ$ -calculus. Theor. Comput. Sci. 27 (1983) 333-354. | Zbl | MR

[20] A. Mader, The modal $μ$ -calculus, model-checking, equations systems and Gauss elimination. TACAS 95 (1995) 44-57.

[21] D. Park, Finiteness is $μ$ -ineffable. Theor. Comput. Sci. 3 (1976) 173-181. | Zbl | MR

[22] H. Seidl, Fast and simple nested fixpoints. Inform. Process. Lett. 59 (1996) 303-308. | Zbl | MR

[23] A. Vincent, 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 :