From CTL to Datalog

We provide a translation from CTL to Datalog¬ Succ. The translation has the following advantages: a) It is natural. b) It provides intuition to the expressive power of CTL and its various fragments. c) It uses a fragment of Datalog¬ Succ which is close to the expressive power of CTL. Categories and Subject Descriptors F.4 [Mathematical Logic and Formal Languages]: Mathematical Logic—temporal logic; I.2.3 [Deduction and Theorem Proving]—logic programming General Terms Theory, verification

• Type: Conference
• Year: 2003
• Where: BIRTHDAY
• Authors: Foto N. Afrati, Theodore Andronikos, Vassia Pavlaki, E. Foustoukos, Irène Guessarian
• Keywords: Applied Computing, BIRTHDAY 2003, Datalog¬ Succ, Expressive Power, Mathematical Logic—temporal Logic