Multi Dimensional CTL and Stratified Datalog

In this work we define Multi Dimensional CTL (MD-CTL in short) by extending CTL which is the dominant temporal specification language in practice. The need for Multi Dimensional CTL is mainly due to the advent of semi-structured data. The common path nature of CTL and XPath which provides a suitable model for semi-structured data, has caused the emergence of work on specifying a relation among them aiming at exploiting the nice properties of CTL. Although the advantages of such an approach have already been noticed [36, 26, 5], no formal definition of MD-CTL has been given. The goal of this work is twofold; a) we define MD-CTL and prove that the "nice" properties of CTL (linear model checking and bounded model property) transfer also to MD-CTL, b) we establish new results on stratified Datalog. In particular, we define a fragment of stratified Datalog called Multi Branching Temporal (MBT in short) programs that has the same expressive power as MD-CTL. We prove that by devising a linear translation between MBT and MD-CTL. We actually give the exact translation rules for both directions. We further build on this relation to prove that query evaluation is linear and checking satisfiability, containment and equivalence are EXPTIME-complete for MBT programs. The class MBT is the largest fragment of stratified Datalog for which such results exist in the literature.