Datalog LITE: a deductive query language with linear time model checking. 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 (mu)-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 extit{stratified} Datalog have too limited expressive power.