On relating CTL to Datalog

Details On relating CTL to Datalog On relating CTL to Datalog

2005-10-04

arxiv.org/abs/cs/0510012v2

Computer Science

Logic in Computer Science

34 pages, 1 figure (file .eps)

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

On relating CTL to Datalog does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On relating CTL to Datalog, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On relating CTL to Datalog will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-83208