CTL is the dominant temporal specification language in practice mainly due to the fact that it admits model checking in linear time. Logic programming and the database query language Datalog are often used as an implementation platform for logic languages. In this paper we present the exact relation between CTL and Datalog and moreover we build on this relation and known efficient algorithms for CTL to obtain efficient algorithms for fragments of stratified Datalog. The contributions of this paper are: a) We embed CTL into STD which is a proper fragment of stratified Datalog. Moreover we show that STD expresses exactly CTL -- we prove that by embedding STD into CTL. Both embeddings are linear. b) CTL can also be embedded to fragments of Datalog without negation. We define a fragment of Datalog with the successor build-in predicate that we call TDS and we embed CTL into TDS in linear time. We build on the above relations to answer open problems of stratified Datalog. We prove that query evaluation is linear and that containment and satisfiability problems are both decidable. The results presented in this paper are the first for fragments of stratified Datalog that are more general than those containing only unary EDBs.
@cite_39: The modal mu-calculus is an expressive logic that can be used to specify safety and liveness properties of concurrent systems represented as labeled transition systems (LTSs). We show that Model Checking in the Modal Mu-Calculus (MCMMC)-the problem of checking whether an LTS is a model of a formula of the propositional modal mu-calculus-is P-hard even for a very restrictive version of the problem involving the alternation-free fragment. In particular, MCMMC is P-hard even if the formula is fixed and alternation-free, and the LTS is deterministic, acyclic, and has fan-in and fan-out bounded by 2. The reduction used is from a restricted version of the circuit value problem known as Synchronous Alternating Monotone Fanout 2 Circuit Value Problem. Specifically, we exhibit NC-algorithms for two potentially useful versions of the problem, both of which involve alternation-free formulas containing a constant number of fixed point operators: 1) the LTS is a finite tree with bounded fan-out; and 2) the formula is A-free and the LTS is deterministic and over an action alphabet of bounded size. In the course of deriving our algorithm for 2), we give a parallel constant-time reduction from the alternation-free modal mu-calculus to Datalog. We also provide a polynomial-time reduction in the other direction thereby establishing an interesting link between the two formalisms. >
@cite_17: 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.
The database query language Datalog has inspired work in @cite_17 , where the language Datalog LITE is introduced. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable occurrences and a limited form of universal quantification in rule bodies. Datalog LITE is shown to encompass CTL and the alternation-free @math -calculus. Research on model checking in the modal @math -calculus is pursued in @cite_39 where the connection between modal @math -calculus and Datalog is observed. This is used to derive results about the parallel computational complexity of this fragment of modal @math -calculus.