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
topHow 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).
- A. Arnold and P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems. Inform. Process. Lett.29 (1988) 57–66.
- 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.
- 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.
- W. Charatonik, D. McAllester, D. Niwínski, A. Podelski and I. Walukiewicz, The horn Mu-calculus. LICS (1998) 58–69.
- 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.
- 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.
- E. Emerson, Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997–1072.
- 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).
- 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.
- 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.
- I. Guessarian, E. Foustoucos, T. Andronikos and F. Afrati, On temporal logic versus Datalog. Theor. Comput. Sci.303 (2003) 103–133.
- M. Jurdzinski, Small progress measures for solving parity games. Proc. STACS'2000 (2000) 290–301.
- M. Jurdzinski, M. Paterson and U. Zwick, A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117–123.
- D. Kozen, Results on the propositional µ-calculus. Theor. Comput. Sci.27 (1983) 333–354.
- 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.
- H. Seidl, Fast and simple nested fixpoints. Inform. Process. Lett.59 (1996) 303–308.
- 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 ?
topYou 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.