ABSTRACT
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 fragments 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 effect that linear-time fragments of stratified Datalog have too limited expressive power.