Properties and Logical Operators

During a run $\varrho_{A}$ of an automaton $A$ are the important informations the $states Q$ of the automaton $A$ with the associated properties as well as the input events bound to the transitions. Input events are often also called actions caused by the environment. In the following semantical interpretations of the $L_{CTL^{*}}$ language the defintions make only use of the properties of the states (atomic propositions). Besides this it is possible -and in some situations necessary- to define also some meaning including possible input or output words.

The properties are given here as a set $L_{PROP}$ of atomic propositions.

If we have an automaton $A$ with a run $\varrho$ we can identify a certain state $q$ of the automaton $A$ by referring to a position i in the execution $\varrho$ of $A$ understood here as time i. It holds $proj_{1}(\varrho(i)) = q$ (e.g. if r is an ordered pair like $r = (a,b)$ then is the first projection of r $proj_{1}(r) = a$).

If a certain property $\Phi$ is in $proj_{1}(\varrho(i)) = q$ -which is the same as $\Phi \in q$- it states that the proposition $\Phi$ is satiesfied by automaton $A$ in run $\varrho$ at time i. Taking the proposition $\Phi$ as an example of an expression of the language $L_{PROP} \subseteq StateFML \subseteq L_{CTL^{*}}$ then one can write

$$A,\varrho,i \models \Phi$$

the expression $\Phi$ is true -or satisfied- at time i in the run $\varrho$ of automaton $A$.

Likewise one can represent the falseness of some $\Phi$ in a certain state of a run of an automaton as

$$A,\varrho,i \models \neg\Phi$$

reading: the expression $\Phi$ is not true -i.e. false- at time i in the run $\varrho$ of automaton $A$. If p is an expression of $L_{PROP}$ then $\neg p$ has to be interpreted as $(p \notin proj_{1}(\varrho(i)))$. Another way of writing would be

$$A,\varrho,i \not\models p$$

It is possible to define the truth of more complex expressions $\Phi, \Phi' \in StateFML \subseteq L_{CTL^{*}}$ if one makes these expressions to arguments of logical operators like (negation, not) $\neg$, (conjunction, and) $\wedge$, and (disjunction, or) $\vee$. It shall hold that with $\Phi, \Phi' \in StateFML \subseteq L_{CTL^{*}}$ then $\neg \Phi$, $\Phi\wedge \Phi'$, and $\Phi\vee \Phi'$are also in $L_{CTL^{*}}$ and it holds

$$A,\varrho,i \models \Phi \wedge \Psi$$

iff $A,\varrho,i \models \Phi$ & $A,\varrho,i \models \Psi$ and

$$A,\varrho,i \models \Phi \vee \Psi$$

iff $A,\varrho,i \models \Phi$ or $A,\varrho,i \models \Psi$