| Issue |
RAIRO-Theor. Inf. Appl.
Volume 43, Number 1, January-March 2009
|
|
|---|---|---|
| Page(s) | 1 - 21 | |
| DOI | https://doi.org/10.1051/ita:2007043 | |
| Published online | 20 December 2007 | |
Inf-datalog, Modal Logic and Complexities
1
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
Received:
18
September
2007
Accepted:
10
October
2007
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 [CITE]. 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).
Mathematics Subject Classification: 68Q19 / 03C13
Key words: Databases / model-checking / specification languages / performance evaluation.
© EDP Sciences, 2008
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.