# Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos; Irène Guessarian

RAIRO - Theoretical Informatics and Applications (2007)

- Volume: 43, Issue: 1, page 1-21
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topFoustoucos, Eugénie, and Guessarian, Irène. "Inf-datalog, Modal Logic and Complexities." RAIRO - Theoretical Informatics and Applications 43.1 (2007): 1-21. <http://eudml.org/doc/92905>.

@article{Foustoucos2007,

abstract = {
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 [CITE].
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 CTL 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).
},

author = {Foustoucos, Eugénie, Guessarian, Irène},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Databases; model-checking; specification languages; performance evaluation.; databases; performance evaluation},

language = {eng},

month = {12},

number = {1},

pages = {1-21},

publisher = {EDP Sciences},

title = {Inf-datalog, Modal Logic and Complexities},

url = {http://eudml.org/doc/92905},

volume = {43},

year = {2007},

}

TY - JOUR

AU - Foustoucos, Eugénie

AU - Guessarian, Irène

TI - Inf-datalog, Modal Logic and Complexities

JO - RAIRO - Theoretical Informatics and Applications

DA - 2007/12//

PB - EDP Sciences

VL - 43

IS - 1

SP - 1

EP - 21

AB -
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 [CITE].
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 CTL 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).

LA - eng

KW - Databases; model-checking; specification languages; performance evaluation.; databases; performance evaluation

UR - http://eudml.org/doc/92905

ER -

## References

top- S. Abiteboul, R. Hull and V. Vianu, Foundations of databases. Addison-Wesley (1995). Zbl0848.68031
- A. Arnold and P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems. Inform. Process. Lett.29 (1988) 57–66. Zbl0663.68075
- A. Arnold and D. Niwiński, Rudiments of µ-calculus. Stud. Logic Found. Math.146, Elsevier Science, North-Holland, Amsterdam (2001).
- J. Bradfield, Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO-Theor. Inf. Appl.33 (1999) 341–356. Zbl0945.68126
- 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. Zbl0901.68118
- W. Charatonik, D. McAllester, D. Niwínski, A. Podelski and I. Walukiewicz, The horn Mu-calculus. LICS (1998) 58–69. Zbl0945.03541
- E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic Verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS8 (1986) 244–263. Zbl0591.68027
- 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. Zbl0772.68038
- E. Emerson, Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997–1072. Zbl0900.03030
- 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). Zbl0877.03020
- 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.
- 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.
- G. Gottlob and C. Koch, Monadic Datalog and the expressive power of web information extraction languages. Proc. PODS'02 (2002) 17–28. Zbl1316.68045
- G. Gottlob, E. Grädel and H. Veith, Datalog LITE: temporal versus deductive reasoning in verification. ACM T. Comput. Log.3 (2002) 39–74.
- A. Griffault and A. Vincent, The Mec 5 model-checker, CAV'04. Lect. Notes Comput. Sci.3114 (2004) 488–491. Zbl1103.68619
- I. Guessarian, E. Foustoucos, T. Andronikos and F. Afrati, On temporal logic versus Datalog. Theor. Comput. Sci.303 (2003) 103–133. Zbl1019.03021
- M. Jurdzinski, Small progress measures for solving parity games. Proc. STACS'2000 (2000) 290–301. Zbl0962.68111
- M. Jurdzinski, M. Paterson and U. Zwick, A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117–123. Zbl1192.91013
- D. Kozen, Results on the propositional µ-calculus. Theor. Comput. Sci.27 (1983) 333–354. Zbl0553.03007
- A. Mader, The modal µ-calculus, model-checking, equations systems and Gauss elimination. TACAS95 (1995) 44–57.
- D. Park, Finiteness is µ-ineffable. Theor. Comput. Sci.3 (1976) 173–181. Zbl0353.02027
- H. Seidl, Fast and simple nested fixpoints. Inform. Process. Lett.59 (1996) 303–308. Zbl0900.68458
- A. Vincent, Conception et réalisation d'un vérificateur de modèles AltaRica. Ph.D. Thesis, LaBRI, University of Bordeaux 1 (2003) URIhttp://altarica.labri.fr/Doc/Biblio/Author/VINCENT-A.html

## NotesEmbed ?

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