The Semantics of $L_{CTL}$- and $L_{CTL^{*}}$-Expressions

Generally, if one wants to interprete the expressions of a formal language $L$ one has to give a mapping from the expressions of the language $L$ into some formal structure $M$ called a Model for the language. If this mapping is done well one can establish a relationship $M \models f$ which says that a certain expression $f$ of the formal language $L$ is $satisfied$ or $fullfilled$ by the model $M$. If the expressions $f$ of $L$ are complex ones built from more simpler ones one has to define the satisfyability relation $\models$ not only for the expression $f$ but also for all possible subformulas of $f$.

In the case of temporal logic languages like $L_{CTL}$ or $L_{CTL^{*}}$ one can assume as possible structures e.g. automata, graphs, kripke structures, algebras etc. From the point of view of computation is the concept of the automaton the most interesting one. For the sake of understandability one uses in connection with automata also the concept of a graph, especially the transition graph of an automaton as well as the execution graph of an automaton (see above).

To construct a mapping from $L_{CTL^{*}}$-expressions into a structure like an automaton $A$ one has to consider three main dimensions: (i) the atomic propositions $L_{PROP}$ (usually representing some properties) associated with some states $Q$ of the automaton $A$, (ii) the runs $\varrho$ of the automaton $A$ -or the corresponding paths $\pi$ of the execution graph of the automaton $A$- or (iii) the whole set of possible executions $exec(A)$ or of $paths(A)$ of the automaton $A$. This will be explained in more detail below. If not otherwise noted it will be assumed that the atomic propositions are embedded in the states, i.e. $Q \subseteq 2^{L_{PROP}}$ is a finite set of P-states.