Treffer: INF-DATALOG, MODAL LOGIC AND COMPLEXITIES
Title:
INF-DATALOG, MODAL LOGIC AND COMPLEXITIES
Authors:
Source:
Informatique théorique et applications (Imprimé). 43(1):1-21
Publisher Information:
Les Ulis: EDP Sciences, 2009.
Publication Year:
2009
Physical Description:
print, 23 ref
Original Material:
INIST-CNRS
Subject Terms:
Control theory, operational research, Automatique, recherche opérationnelle, Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences et techniques communes, Sciences and techniques of general use, Mathematiques, Mathematics, Logique mathématique, fondements, théorie des ensembles, Mathematical logic, foundations, set theory, Logique et fondements, Logic and foundations, Logique générale, General logic, Analyse mathématique, Mathematical analysis, Analyse fonctionnelle, Functional analysis, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie des langages et analyse syntaxique, Language theory and syntactical analysis, Divers, Miscellaneous, Application, Aplicación, Base de données, Database, Base dato, Calcul automatique, Computing, Cálculo automático, Complexité espace, Space complexity, Complejidad espacio, Complexité linéaire, Linear complexity, Complejidad lineal, Complexité programme, Program complexity, Complejidad programa, Complexité temps, Time complexity, Complejidad tiempo, DATALOG, Espace linéaire, Linear space, Espacio lineal, Evaluation performance, Performance evaluation, Evaluación prestación, Informatique théorique, Computer theory, Informática teórica, Langage spécification, Specification language, Lenguaje especificación, Logique modale, Modal logic, Lógica modal, Noeud, Node, Nudo, Performance, Rendimiento, Polynôme, Polynomial, Polinomio, Preuve, Proof, Prueba, Profondeur, Depth, Profundidad, Requête, Query, Pregunta documental, Spécification, Specification, Especificación, Sémantique, Semantics, Semántica, Temps linéaire, Linear time, Tiempo lineal, Temps polynomial, Polynomial time, Tiempo polinomial, 03B45, 46Axx, 68M20, 68P15, 68Q55, 68Q60, Complexité donnée, Puissance expressive, 03C13. Databases, 68Q19, model-checking, performance evaluation, specification languages
Document Type:
Fachzeitschrift
Article
File Description:
text
Language:
English
Author Affiliations:
MPLA, National and Capodistrian University of Athens, Department of Mathematics, Panepistimiopolis, 15784 Athens, Greece
LIAFA, UMR 7089, Université Paris 7, case 7014, 2 Place Jussieu, 75251 Paris, France
LIAFA, UMR 7089, Université Paris 7, case 7014, 2 Place Jussieu, 75251 Paris, France
ISSN:
0988-3754
Rights:
Copyright 2009 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Mathematics
Mathematics
Accession Number:
edscal.20912509
Database:
PASCAL Archive
Weitere Informationen
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μk (modal μ-calculus with fixed alternation-depth at most k).