|
Abstract : |
We present Datalog LITE, a new deductive query language with a linear time model checking algorithm, i.e., linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratied negation, restricted variable occurrences and a limited form of universal quantication 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 xed point logic. Consequently, linear time model checking algorithms for all mentioned logics are obtained in a unied way. The results are complemented by inexpressibility proofs to the eect that linear time fragments of stratied Datalog have too limited expressive power., |
