Τίτλος:
Inf-datalog, modal logic and complexities
Γλώσσες Τεκμηρίου:
Αγγλικά
Περίληψη:
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.
Συγγραφείς:
Foustoucos, E.
Guessarian, I.
Περιοδικό:
RAIRO - Theoretical Informatics and Applications
Λέξεις-κλειδιά:
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
