TY - JOUR
TI - Inf-datalog, modal logic and complexities
AU - Foustoucos, E.
AU - Guessarian, I.
JO - RAIRO - Theoretical Informatics and Applications
PY - 2009
VL - 43
TODO - 1
SP - 1-21
PB - 
SN - 0988-3754, 1290-385X
TODO - 10.1051/ita:2007043
TODO - Calculations;  Differentiation (calculus);  Information theory;  Semantics;  Specification languages, Data complexities;  Databases;  Elementary proofs;  Expressive powers;  Finite models;  Fixpoint semantics;  Global models;  Linear programs;  Modal logics;  Performance evaluation;  Program complexities;  Query evaluations, Model checking
TODO - 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 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μκ (modal μ-calculus with fixed alternation-depth at most κ). © 2007 EDP Sciences.
ER -