6
$\begingroup$

Background:
In the book of Principles of Model Checking (Christel Baier and Joost-Peter Katoen, MIT Press, 2007), Section 9.2, page 701, the semantics of the until modality is defined over some time-divergent path $\pi \in s_0 \Rightarrow^{d_0} s_1 \Rightarrow^{d_1} \cdots \Rightarrow^{d_{i-1}} s_i \Rightarrow^{d_i} \cdots$ as follows:

(We can skip the formal definition at your first reading.)
$\pi \models \Phi \cup^{J} \Psi \iff$
$\exists i \ge 0. s_i + d \models \Psi \textrm{ for some } d \in [0,d_i] \textrm{ with } \sum_{k=0}^{i-1}d_k + d \in J \textrm{ and }$ $\forall j \le i. s_j + d' \models \Phi \lor \Psi \textrm{ for any } d' \in [0,d_j] \textrm{ with } \sum_{k=0}^{j-1} d_k + d' \le \sum_{k=0}^{i-1} d_k + d$.

Intuitively, time-divergent path $\pi \in s_0 \Rightarrow^{d_0} s_1 \Rightarrow^{d_1} \cdots \Rightarrow^{d_{i-1}} s_i \Rightarrow^{d_i} \cdots$ satisfies $\Phi \cup^{J} \Psi$ whenever at some time point in $J$, a state is reached satisfying $\Psi$ and at all previous time instants $\Phi \lor \Psi$ holds.

However, in the book of Model Checking by E.M. Clarke (Section 16.3, Page 256), the semantics of the until modality is given as follows:

$s \models E[\Phi \cup_{[a,b]} \Psi]$ if and only if there exists a path $\pi = s_0 s_1 s_2 \cdots$ starting at $s = s_0$ and some $i$ such that $a \le i \le b$ and $s_i \models \Psi$ and for all $j < i, s_j \models \Phi$.

As indicated, the second definition is stricter than the first one in that it does not allow the case of $\lnot \Phi \land \Psi$ before reaching a state satisfying $\Psi$.

Questions:

  1. Why are there two different until ($\cup$) semantics in Timed Computation Tree Logic (TCTL)?

  2. Which one is more official?

$\endgroup$
2
$\begingroup$

The two definitions are equivalent:

As you point out, the second one implies the first, as if $\phi$ holds, then clearly $\phi\vee \psi$ holds.

Conversely, consider a computation that satisfies the first definition, and assume by way of contradiction that it does not satisfy the second definition. Thus, there exists some time in which $\psi$ holds, and in all previous times, $\psi\vee \phi$ holds. However, there also exists a previous time $d$ where $\psi\wedge \neg \phi$ holds, otherwise the second definition would hols.

Consider the minimal (or infimum) time $d$ for which this happens. Then in that time, $\psi$ holds, and in all previous times, $\psi\wedge \phi$ holds, so the second definition also holds for time $d$, which implies it for any later time.

Another way of looking on it: assume that the second definition doesn't hold, so either $\psi$ never holds, in which case clearly the first definition fails, or there is some minimal time $d$ where $\phi$ doesn't hold, and $\psi$ doesn't hold before $d$. In the latter case, $\phi\vee \psi$ also doesn't hold at time $d$, so the first definition doesn't hold.

$\endgroup$
  • $\begingroup$ Thanks. However, in your last statement, "in that time, $\psi$ holds, and in all previous time, $\psi \lor \phi$ holds, so the second definition also holds for time $d$", is it the first definition? Furthermore, following your argument, I think they are equivalent if and only if the path is $\pi = \psi \psi \psi \cdots$ (i.e., $\pi \models \Box \psi$). $\endgroup$ – hengxin Dec 29 '13 at 2:42
  • $\begingroup$ Sorry, it should have said $\psi\wedge \phi$. I corrected it. $\endgroup$ – Shaull Dec 29 '13 at 6:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.