Timed CTL: TCTL and tCTL

(Has to be rewritten because the semantics has changed)

If one accepts the assumption that the execution time $c$ of an automaton can be zero than one has the problem how to manage the dense real-time points within the system. In this case a run becomes a mapping from the real numbers $\cal{R}$ into the set of possible states organized as an execution. Because in this scenario a definite succesor of a processing state q at time point t does no longer exist, because there can be infinite many possible time points as successors, one changed the definitions of CTL in a way, that in the extended version timed CTL (TCTL) the description of a run can be done without an explicit next operator X.

The other difference between CTL and TCTL is given by the fact that you can in TCTL extend the quantified formulas as follows:

$$QF_{(\sim k)} \phi$$

or

$$QG_{(\sim k)} \phi$$

or

$$Q\phi U_{(\sim k)} \psi$$

where $Q = \{\exists,\forall\}$, $\sim = \{<, >, \le, \ge\}$, and $k$ any fraction of integers like $7/990$.

This means e.g. that an expression like $\exists \phi U_{\le 5} \psi$ does not only talk about an execution $\varrho$ where you have two different properties $\phi$ at position $t'$ and $\psi$ at position $t$ with $t' < t$, but you can also give a numerical bound with $\le 5$. This numerical bound means that the property $\psi$ has to be reached in the run latest after 5 time units.

Because we are holding in this course the assumption that the processing time $c$ is always greater than zero we do not really need this special version of TCTL. Otherwise the explicit numerical bound $(\sim k)$ has some practical flavor. Therefore we will define here a variant of timed CTL which is between CTL and TCTL, we call it tiny temporal CTL (tCTL). In the tiny CTL specification language we have all expressions from TCTL, but the main difference is that the indices used in tCTL correspond in the model structure $\cal{M}$ to the operation cycles of the automaton (the above mentioned discrete automata time, DAT).

Before we define the syntax and semantics for the tCTL-expressions we have to extend our definition for the automaton with clocks by an additional term for properties, because the tCTL-expressions presuppose the existence of properties connected to the states.

Def.: Automata with Clocks and Properties

$$\langle Q, I, F, \Sigma, \Xi, \Delta , l, AP \rangle$$

with

$$\Delta \subseteq Q \times \Sigma^{*} \times \Gamma \times \Xi^{*} \times Q$$

and

$$l: Q \longrightarrow 2^{AP}$$

Thus, if we have a run $\varrho$ of the automaton then we can deduce from this run for every state the set of attached properties as well as the implied output. We can then use the set of all possible executions $\cal{E}_{\alpha}$ of th automaton alpha as our model $\cal{M}$ to define an interpretation relation for an tCTL-expression $f$ like

$${\cal M} \models f$$

.

• $AP \subseteq tCTL$
• If $\phi,\psi$ $\in AP$ then $\{\neg \phi, \phi \wedge \psi, \phi \vee \psi, \phi \Rightarrow \psi\} \subseteq AP$
• $QF_{(\sim k)} \phi$ or $QG_{(\sim k)} \phi$ or $Q\phi U_{(\sim k)} \psi$ with $Q = \{\exists,\forall\}$, $\sim = \{<, >, \le, \ge\}$, and $k \in {\cal N}$ (We assume a weaker version than usual assumed for TCTL!)..
• ${\cal M} \models \phi$ iff there is a state s $in$ Q which occurs in a run of $\cal{E}$ and $\phi \in l(q)$
• ${\cal M} \models \neg \phi$ iff there is no state s $in$ Q with $\phi \in l(q)$
• ${\cal M} \models \phi \wedge \psi$ iff ${\cal M} \models \phi$ and ${\cal M} \models \psi$
• ${\cal M} \models \phi \vee \psi$ iff ${\cal M} \models \phi$ or ${\cal M} \models \psi$
• ${\cal M} \models \phi \Rightarrow \psi$ iff $\neg( {\cal M} \models \phi$) or ${\cal M} \models \psi$

• $\textbf{F}_{(\sim k)}\phi$ (there is a state coming up in the execution having property $\phi$, but the upcoming occurence must agree with the numerical bound): There is a run $\varrho$. From a point of time $i$ onwards there can be another point of time $j$ with $i < j$ and $j-i \sim k$ and at $j$ there is a state $s = proj_{1}(\varrho_{j})$ and $\phi \in l(s)$. Also written as
  $${\cal M} \models \textbf{F}_{(\sim k)}\phi iff \exists( i,j) i,... ...m(\varrho) \& i < j \& j-i \sim k \& ({\cal M}, \varrho, j) \models \phi$$

• $\textbf{G}_{(\sim k)}\phi$ (all upcoming possible states having property $\phi$, but the upcoming occurence must agree with the numerical bound ): There is a run $\varrho$. From a point of time $i$ onwards all indices $j \in dm(\varrho)$ with $i \le j$ are valid and must agree as $j \sim k$. Every index $j$ identifies with $proj_{1}(\varrho_{j}) = s$ a state $s$ with $\phi \in l(s)$. Also written as
  $${\cal M} \models \textbf{G}_{(\sim k)}\phi iff \exists(i) \for... ...) i,j \in dm(\varrho) \& i \le j \& ({\cal M}, \varrho, j) \models \phi$$

• $\phi \textbf{U}_{(\sim k)} \psi$ (at point j is property $\psi$ true and before j until some k property $\phi$, but the upcoming occurence at j must agree with the numerical bound): There is a run $\varrho$. From a point of time $i$ onwards there can be another point of time $j$ with $i < j$ and $j-i \sim k$ and at $j$ there is a state $s = proj_{1}(\varrho_{j})$ and $\psi \in l(s)$.There is a $k$ with $i \le k < j$ and there is a state $s' = proj_{1}(\varrho_{k})$ and $\phi \in l(s')$. Also written as
  $${\cal M} \models \phi\textbf{U}_{(\sim k)}\psi iff \exists(i,k... ...& ({\cal M}, \varrho, k)\models \phi \& ({\cal M}, \varrho, j)\models \psi$$

Example: We merge the automaton having properties like those in figure 3.4 with an automaton having clocks (cf. figure 5.4).

$$\alpha_{1} = \langle Q, I, F, \Sigma, \Xi, \Delta , \Gamma, l, AP \rangle$$

with

$$\Delta \subseteq Q \times \Sigma^{*} \times \Gamma \times \Xi^{*} \times Q$$

and

$$l: Q \longrightarrow 2^{AP}$$

1. $Q$ = $\{ 1,2,3,4 \}$
2. $I = \{ 1\}$
3. $F = \{ 4\}$
4. $\Sigma$ = $\{ A,B,C, 0-9, \}$.
5. $\Xi$ = $\{ 0-9, \}$
6. $AP$= $\{ start, K=A, K=B \}$.
7. $l$ = $\{ (1,\{ start\}), (2,\{ K=A\}), (3,\{ K=B\}), (1,\{ K=A\}),\}$.

1. $Delta =$
2. $\langle q = 1, in = \langle X_{0}, B, X_{last}, X_{0.LastUpdate(X)}\rangle,\ga... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
3. $\langle q = 1, in = \langle X_{0}, C, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
4. $\langle q = 1, in = \langle X_{0}, A, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...t = \langle q'=2, X_{last}, X_{0.LastUpdate(X)}, X := 0 \rangle , q' = 2\rangle$

5. $\langle q = 2, in = \langle X_{0}, A, X_{last}, X_{0.LastUpdate(X)}\rangle,\ga... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
6. $\langle q = 2, in = \langle X_{0}, C, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
7. $\langle q = 2, in = \langle X_{0}, B, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...t = \langle q'=3, X_{last}, X_{0.LastUpdate(X)}, X := 0 \rangle , q' = 3\rangle$

8. $\langle q = 3, in = \langle X_{0}, B, X_{last}, X_{0.LastUpdate(X)}\rangle,\ga... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
9. $\langle q = 3, in = \langle X_{0}, C, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...out = \langle 1, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 1\rangle$
10. $\langle q =3, in = \langle X_{0}, A, X_{last}, X_{0.LastUpdate(X)} \rangle,\ga... ...t = \langle q'=4, X_{last}, X_{0.LastUpdate(X)}, X := 0 \rangle , q' = 4\rangle$

11. $\langle q = 4, in = \langle X_{0}, A, X_{last}, X_{0.LastUpdate(X)}\rangle,\ga... ...out = \langle 4, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 4\rangle$
12. $\langle q = 4, in = \langle X_{0}, C, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...out = \langle 4, X_{last}, X_{0.LastUpdate(X)},\epsilon \rangle , q' = 4\rangle$
13. $\langle q = 4, in = \langle X_{0}, B, X_{last}, X_{0.LastUpdate(X)} \rangle,\g... ...t = \langle q'=4, X_{last}, X_{0.LastUpdate(X)}, X := 0 \rangle , q' = 4\rangle$

We want to check whether the following tCTL-formula is valid for this concrete automaton:

Question:

$${\cal E}_{\alpha_{1}} \models \textbf{EF}_{(\le 4)} (K = A)$$

Answer: We construct a run $\varrho_{\alpha_{1}} \in {\cal E}_{\alpha_{1}}$ as follows (we write the complete state description to show why the run is working):

1. $\langle q = 1, in = \langle 0,A, 0, 0 \rangle,\gamma = 0 < 3 , out = \langle 2, 1,0, x := 0 \rangle , q' = 2\rangle$
2. $\langle q = 2, in = \langle 1,B, 0,0 \rangle,\gamma = 0 < 3, out = \langle 3, 2, 1, x := 0 \rangle , q' = 3\rangle$
3. $\langle q = 3, in = \langle 2,A, 0, 1 \rangle,\gamma = 0 < 3, out = \langle 4, 3, 2, x := 0 \rangle , q' = 4\rangle$
4. $\langle q = 4, in = \langle 3,C, 0, 2 \rangle,\gamma = \epsilon, out = \langle 4, 4, 3, \epsilon \rangle , q' = 4\rangle$

This shows the following: there is a run $\varrho_{\alpha_{1}}$. There is a position $j = 4$ with state $4$ and according to $l(4)$ we have there the attached property $K=A$. Furthermore does hold $j \le 4$. therefore we can conclude that the tCTL-formula $\textbf{EF}_{(\le 4)} (K = A)$ is satisfied in ${\cal E}_{\alpha_{1}}$, i.e. the formula $\textbf{EF}_{(\le 4)} (K = A)$ is true in the model.