Quantifier

Until now we can only talk about states and properties of states as well as about temporal relations within a run -whereby we remember that a run can be represented as a path in an execution graph-. But we know also that an automaton usually can have more than only one run and that these runs are different. Therefore we assume the set $exec(A)$ as the smallest set of executions of an automaton $A$ with the assumption that for all $\varrho, \varrho' \in exec(A)$ it holds that $\varrho \ne \varrho'$. To be able to talk about the smallest set of all possible executions of automaton A $exec(A)$ -or likewise about the set of all paths within the execution graph based on the automaton A- we need additional operators. These operators are called quantifiers or -because they are applied to formulas from the set of path formulas PathFML- also path operators. Usuall these are the following ones:

If one wants to say that a certain $L_{CTL^{*}}$ expression $\Phi$ shall only be valid in at least one of the possible executions -only in one of the possible paths- then one writes

$$A \models \textbf{E}\Phi iff \exists\varrho, i (\varrho \in exec(A) \& A,\varrho,i \models \Phi)$$

And the complement would be, if we want to say that a certain $L_{CTL^{*}}$ expression $\Phi$ shall be valid in all of the possible executions - in all of the possible paths- then one writes

$$A \models \textbf{A}\Phi iff \forall\varrho(\varrho \in exec(A) \Rightarrow \exists i(i \in dm(\varrho) \& A,\varrho,i \models \Phi))$$

It holds the equivalence:

$$\textbf{A}\Phi iff \neg\textbf{E}\neg\Phi$$