patternMinor
Why are there two different `until` ($\cup$) semantics in Timed Computation Tree Logic?
Viewed 0 times
whytimeduntilsemanticsarecomputationlogicdifferenttwocup
Problem
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
-
Which one is more official?
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
-
Which one is more official?
Solution
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.
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.
Context
StackExchange Computer Science Q#19338, answer score: 2
Revisions (0)
No revisions yet.