Sunday, May 10, 2015

CTL - Computation Tree Logic

In the previous posts we have been talking about Linear Temporal Logic formulas, but there is another kind of temporal logic that allows expressing properties such as "there exists a path starting from  ... ". In CTL (Computation Tree Logic), the temporal operators are the same as in LTL (X, U, G, F), and includes quantifiers (A, E) which express "for every path" or "exists path" respectively.
Then, valid formulas are those that include: Quantifier + Temporal Operator

Examples:
AX p : In every path, the next state satisfies p
EX p : There is a path such that the next state satisfies p

Then the following model:
satisfies the property EX p (there is a path starting from the first state such that in the next state p holds), but it doesn't satisfy AXp (the path that continues below doesn't have p in the next state).

The temporal operators can be combined with boolean ones to build more complex formulas, for example

E(p U AX q) : there is a path where p holds until one state where every next state satisfies q.

Challenge: 
1) for what CTL formula there isn't an LTL equivalent formula ?
2) for what LTL formula there isn't a CTL equivalent formula ?

No comments:

Post a Comment