Document RAIRO-Theor. Inf. Appl. (2008)
DOI: 10.1051/ita:2007043
Inf-datalog, modal logic and complexities
Eugénie Foustoucos1 and Irène Guessarian21 MPLA, National and Capodistrian University of Athens, Department of Mathematics, Panepistimiopolis, 15784 Athens, Greece; aflaw@otenet.gr
2 LIAFA, UMR 7089, Université Paris 7, case 7014, 2 Place Jussieu, 75251 Paris Cedex 5, France; ig@liafa.jussieu.fr
(Published online: 20 December 2007)
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 [I. Guessarian et al. Theor. Comput. Sci. 303 (2003) 103-133].
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 
(modal -calculus with fixed alternation-depth at most k).
Mathematics Subject Classification. 68Q19, 03C13
Key words: Databases -- model-checking -- specification languages -- performance evaluation
© EDP Sciences 2008