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

Question

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?

Answer 1

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.