[Back]

G. Gottlob, E. Grädel, H. Veith:
"Datalog LITE: a deductive query language with linear time model checking";
ACM Transactions on Computational Logic, Volume 3 (2002), 1; 42 - 79.

We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable occurrences and a limited form of universal quantification in rule bodies.
Despite linear-time evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics such as CTL or the alternation-free μ-calculus. In fact, these formalisms have natural presentations as fragment of Datalog LITE: Further, Datalog LITE is equivalent to the alternation-free portion of guarded fixed-point logic. Consequently, linear-time model checking algorithms for all mentioned logics are obtained in a unified way.
The results are complemented by inexpressibility proofs to the linear-time fragments of stratified Datalog have too limited expressive power.