On relating CTL to Datalog

TL;DR

This paper establishes a precise relationship between CTL and Datalog, demonstrating how CTL can be embedded into specific Datalog fragments, leading to efficient algorithms for query evaluation, containment, and satisfiability.

Contribution

It introduces linear embeddings of CTL into stratified Datalog fragments, proving their equivalence and decidability of key problems, advancing understanding of logic programming and temporal logic.

Findings

CTL can be embedded into STD, a fragment of stratified Datalog, with linear complexity.

Embedding CTL into TDS, a Datalog fragment with successor, is also linear.

Query evaluation in these Datalog fragments is linear, and containment and satisfiability are decidable.

Abstract

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.