Inf-datalog, Modal Logic and Complexities
MPLA, National and Capodistrian University of Athens,
Department of Mathematics, Panepistimiopolis, 15784
Athens, Greece; email@example.com
2 LIAFA, UMR 7089, Université Paris 7, case 7014, 2 Place Jussieu, 75251 Paris Cedex 5, France; firstname.lastname@example.org
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