Inf-datalog, Modal Logic and Complexities

Issue		RAIRO-Theor. Inf. Appl. Volume 43, Number 1, January-March 2009


Page(s)		1 - 21
DOI		10.1051/ita:2007043
Published online		20 December 2007

RAIRO-Theor. Inf. Appl. 43, 1-21 (2009)
DOI: 10.1051/ita:2007043

Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos¹ and Irène Guessarian²

¹ MPLA, National and Capodistrian University of Athens, Department of Mathematics, Panepistimiopolis, 15784 Athens, Greece; aflaw@otenet.gr
² LIAFA, UMR 7089, Université Paris 7, case 7014, 2 Place Jussieu, 75251 Paris Cedex 5, France; ig@liafa.jussieu.fr

Received September 18, 2007. Accepted October 10, 2007 Published online 20 December 2007

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 $\mu$ -calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for $L\mu_k$ (modal $\mu$ -calculus with fixed alternation-depth at most k).

Mathematics Subject Classification. 68Q19, 03C13

Key words: Databases -- model-checking -- specification languages -- performance evaluation.

© EDP Sciences 2007

What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.