Specification Language CTL

To talk about these properties in a way, which would be 'understandable' by an automatic property proofer, one will need a formal language $\cal L$ which allows statements about such properties and which can be computed by an automaton. Languages which are commonly used for such tasks are often taken from temporal logic, especially the language CTL (short for Computational Tree Logic).

In CTL you have expressions for properties like those above. But you can also connect properties with logical connectors like $\neg$ (negation), $\wedge$ (and, conjunction), $\vee$ (or, disjunction). This generates expressions like $K=A \vee K=B \wedge \neg (K=C)$. Expressions with properties and logical connectors are called state expressions, because you can describe which properties a state should have. Looking to a path $\sigma$ of an execution graph $\cal G'$ you have a sequence of states which are labled with consecutive numbers from 0 to some $n$ in the finite case and to some $\omega$ in the infinite case. If one interpretes these numbers as points in time then one can interprete every path as a time line with an order which allows the definition of functions like predecessor (pred) and successor (succ), where $succ(i) = i+1$ and $pred(i) = i-1$ as long $i-1, i+1$ are still part of the sequence $\sigma$.

Based on these assumptions one can introduce further language expressions of CTL which will be called Temporal Operators like X (the successor of some i in a path, $succ(i)$), F ('future': there is some j in the path greater than the actual i), G (global: for all elements of the actual path), and U (until: there is a j in the path and from an actual i until this j there is something else). The temporal operators take as arguments state expressions and generate path expressions. They are talking about a whole path $\sigma$.

For our toy example we could specify questions like the following ones:

1. $start$ := Is there a state (= vertex) in the whole execution graph $\cal G'$ which has the property $start$?
2. $K=A \wedge K=B$ := Is there a state in the whole execution graph $\cal G'$ which has the two properties 'K=A' and 'K=B' at the same time?
3. $K=A \vee K=B \vee K=C$ := Is there a state in the whole execution graph $\cal G'$ which has at least one of the properties 'K=A' or 'K=B' or 'K=C'?
4. X$K=A$ := is there a path in the whole execution graph $\cal G'$ which has a position i followed by a position i+1 where we have at i+1 a state which has the property 'K=A'?
5. F$K=B$ := is there a path in the whole execution graph $\cal G'$ which has a position j following the actual position i where we have at j a state which has the property 'K=B'?
6. G$K=C$ := is there a path in the whole execution graph $\cal G'$ which has at all positions states which have the properties 'K=C'?
7. $K=A$U$K=B$ := is there a path in the whole execution graph $\cal G'$ which has a position j with a state with property 'K=B' and before this j a position i such, that all states from position i until position j-1 have the property 'K=A'?

And CTL has even more operators. Commonly used are E (exist:for at least one path in the whole execution graph $\cal G'$) and A(all: for all pathes in the whole execution graph $\cal G'$). These quantifiers are taking path expressions as arguments and generate again state expressions.

For our toy example we could specify questions like the following ones:

1. EX$K=A$ := is there at least one path in the whole execution graph $\cal G'$ which has a position i followed by a position i+1 where we have at i+1 a state which has the property 'K=A'?
2. AX$K=A$ := Does it hold for all pathes in the execution graph $\cal G'$ that we have a position i followed by a position i+1 where we have at i+1 a state which has the property 'K=A'?
3. EF$K=B$ := is there at least one path in the whole execution graph $\cal G'$ which has a position j following the actual position i where we have at j a state which has the property 'K=B'?
4. AF$K=B$ :=Does it hold for all pathes in the execution graph $\cal G'$ that there is a position j following the actual position i where we have at j a state which has the property 'K=B'?
5. EG$K=C$ := is there at least one path in the whole execution graph $\cal G'$ which has at all positions states which have the properties 'K=C'?
6. AG$K=C$ :=Does it hold for all pathes in the execution graph $\cal G'$ that there are at all positions of each graph states which have the properties 'K=C'?
7. E($K=A$U$K=B$):= is there at least one path in the whole execution graph $\cal G'$ which has a position j with a state with property 'K=B' and before this j a position i such, that all states from position i until position j-1 have the property 'K=A'?
8. A($K=A$U$K=B$):= Does it hold for all pathes in the execution graph $\cal G'$ that there are positions j with a state with property 'K=B' and before this j a position i such, that all states from position i until position j-1 have the property 'K=A'?

These expressions look nice, but CTL has its limits. To express in CTL, that there exist a path $\sigma$ in the execution graph $\cal G'$ whose last three vertices have the properties $K=A, K=B, K=A$, this is not possible! One ca say E$K=A$U$K=B$ or E$K=B$U$K=A$, but one cannot repeat temporal operators without an additionl quantifier converting a path expression into a state expression! And to say E$K=A$U$K=B$ $\wedge$ E$K=B$U$K=A$ is not the same, because each of the expressions E$K=A$U$K=B$ and E$K=B$U$K=A$ can describe a different path.

In the toy example it would -luckily- be enough to check whether there is a path $\sigma$ with a vertex with property 'K=A' preceeded by a state with property 'K=B' as E((K=B)U(K=A)). If we would introduce the property 'final' related to final states, then the test for a possible solution would become very simple.