@article{3065012,
    title = "Inf-datalog, modal logic and complexities",
    author = "Foustoucos, E. and Guessarian, I.",
    journal = "RAIRO - Theoretical Informatics and Applications",
    year = "2009",
    volume = "43",
    number = "1",
    pages = "1-21",
    issn = "0988-3754, 1290-385X",
    doi = "10.1051/ita:2007043",
    keywords = "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",
    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 [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."
}