Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / The Benefits of Relaxing Punctuality
Tags: hasSeenConjDef récupéré TypToQuestion fromMath omitted

Definition: The left end-point of \(I\)
Page: 118
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(I\) an interval
Notation: \(l(I)\)

Name: The right end-point of \(I\)
Page: 118
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(I\) an interval
Abbreviation: \(r(I)\)

Name: A singular interval
Definition: A singleton, considered as an interval
Page: 118
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1

Name: Adjacent interval
Definition: Disjoint interval whose union is an interval
Page: 118
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1

Name: An interval sequence
Definition: initiality
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Index: 1
Kind: Def
Definition2: adjacency
Conjdef: An infinite sequence of time interval which satisfies the properties
Definition3: progress
Denoted by: \(\overline I\)

Name: A sequence of time intervals satisfying the initiality property
Definition: A sequence of time intervals \((I_i)_{i\in\mathbb N}\) such that \(I_0\) is \([0,a]\) or \([0,a)\).
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Index: 1
Kind: Def

Name: A sequence of time intervals satisfying the adjacency property
Definition: A sequence of time intervals \((I_i)_{i\in\mathbb N}\) such that \(I_i\) is adjacent to \(I_{i+1}\).
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Index: 1
Kind: Def

Name: A sequence of time intervals satisfying the progress property
Definition: A sequence of time intervals \((I_i)_{i\in\mathbb N}\) such that for each \(t>0\), \(t\in I_i\) for some \(i\ge 0\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Index: 1
Kind: Def

Name: A timed state sequence
Definition: A pair with a time sequence and a state sequence
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Notation: \((s_{0},I_0)\to(s_{1},I_{1})\to\dots \)
Index: 1
Kind: Def
Denoted by: \(\tau\)

Name: The state at time \(t\)
Definition: A state \(s_i\) such that \(t\in I_i\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence
\(\tau=(\overline s,\overline I)\) a timed state sequence,
\(t\ge0\)
Notation: \(\tau^*(t)\)
Index: 1
Kind: Def

Name: Equivalent time sequences
Definition: Times sequences \(\tau\) and \(\tau'\) such that \(\tau^*\) equals \(\tau^{\prime *}\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Index: 2
Kind: Def

Definition: \((s_{i},I_i)\to(s_{i+1},I_{i+1})\to\dots \)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence
Notation: \((s,\bigcup_{j\ge i}I_j)\)

Name: A transition point
Definition: The left end-point of some \(I_i\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence

Name: A singular state in \(\tau\)
Definition: A state \(s_i\) such that \(I_i\) is singular
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \)

Smaller0: \(s_{i+1}\) is non singular
Greater0: \(s_i\) is non singular
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
\(i\in\mathbb N\)
Smaller to greater: or
Hide sides: yes

Name: The suffix of \(\tau\) at time \(t\)
Definition: \((s_j,T_j-t)_{j\ge i}\), where \(t\in I_i\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
\(t\in I_i\)
Notation: \(\tau^t\)
Index: 3
Kind: Def

Question: \(\tau^0=\)
Answer: \(\tau\)
Page: 119
Chapter: The Benefits of Relaxing Punctuality
Section: 2.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
Index: 3
Kind: Def

Name: Next
Page: 120
Chapter: The Benefits of Relaxing Punctuality
Section: 3.1
Context: MITL with continuous semantic
Typ: does not exists

Question: In \(\tau\models\phi\mathcal U\psi\), what should hold at time 0 ?
Answer: Nothing is required.
Page: 120
Chapter: The Benefits of Relaxing Punctuality
Section: 3.1

Definition: There exists \(t\in I\) such that \(\tau^t\models\psi\) and for each \(0<t'<t\), \(\tau^{t'}\models\phi\)
Page: 120
Chapter: The Benefits of Relaxing Punctuality
Section: 3.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
\(\phi,\psi\) MITL formulae
Context: Continuous semantic
Notation: \(\tau\models\phi\mathcal U_I\psi\)

Question: Difference of \(\tau\models\phi\mathcal U_I\psi\) in continuous/discrete semantic
Answer: Time 0 may be considered in continuous semantic if it belongs to \(I\)
Page: 120
Chapter: The Benefits of Relaxing Punctuality
Section: 3.1
Variables: \(\overline I=(I_i)_{i\in\mathbb N}\) an interval sequence
\(\overline s=(s_i)_{i\in\mathbb N}\) a state sequence,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
\(\phi,\psi\) MITL formulae
Answer2: In continuous, there is no next operator
Answer3: Absence of subscript indicates \((0,\infty)\) for continuous, and \([0,\infty)\) for discret

Smaller0: \(\tau^0\) and \(\tau^1\) are equivalent
Greater0: \(\tau^0\models\phi\iff\tau^1\models\phi\)
Page: 120
Chapter: The Benefits of Relaxing Punctuality
Section: 3.1
Variables: \(\overline I^j=(I_i^j)_{i\in\mathbb N}\) an interval sequence
For \(j\) being 0 or 1,
\(\overline s^j=(s_i^j)_{i\in\mathbb N}\) a state sequence,
\(\tau^j=(s_{0}^j,I^j_0)\to(s^j_{1},I^j_{1})\to\dots \),
Let \(\phi\) a MITL formulae
Index: 2
Kind: Rem

Name: A timed-state sequence satisfying the finite-variability condition.
Definition: A timed-state sequence such that, in any finite interval, there is a finite number of state change.
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Definition2: \(\forall t\exists t 1[(t<t_1)\land t_2(t<t_2<t_1)\to (X(t_2)\iff X(t_1)]\land\forall t>0\exists t_1[(t_1<t)\land\forall t_2(t_1<t_2<t)\to(X(t_2)\iff X (t_1)]\)

Name: A \(\phi\)-fine timed state sequence
Definition: A timed-sequence \(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), such that for all subformulas \(\psi\) of \(\phi\), for all \(i\ge0\) and for all \(t,t'\in I_i\), \(\tau^t\models\psi\) iff \(\tau^{t'}\models\psi\).
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) an MITL formula
Index: 1
Kind: Def

Question: \(\tau_{\neg\phi}\)
Answer: equals \(\tau_\phi\)
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formula,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem

Definition: A \(\phi\)-fine time-sequence equivalent to \(\tau\)
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formula,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a timed state sequence satisfying the finite-variability condition
Notation: \(\tau_{\phi}\)
Index: 2
Kind: Lem

Question: \(\tau_{\phi^1\land\phi^2}\)
Answer: equals the refinment of \(\tau_{\phi^1}\) and \(\tau_{\phi^2}\)
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi^1,\phi^2\) a MITL formulas,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem

Definition: a transition point of \(\tau_{\phi^1\land\phi^2}\), or
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi^1,\phi^2\) a MITL formulas,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem
Definition2: \(\tau\) satisfies the finite-variability condition
Conjdef: \(([t_i,t_i],(t_i,t_{i+1}))_{i\in\mathbb N}\) where \((t_i)\in\mathbb R^{\ge0}\) the increasing sequence containing
Extra: Check I
Denoted by: \(\tau_{\phi^1\mathcal U_I\phi^2}\)

Name: A rational timed-sequence
Definition: A timed-sequence whose transition points are rational.
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1

Name: \(\phi\) \(\mathbb Q\)-satisfies \(\tau\)
Definition: \(\phi\models\tau\) where the quantifications are restricted to rational numbers.
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1
Variables: \(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a rational timed state sequence
\(\phi\in MITL\)

Name: A \(\mathbb Q\)-satisfiable formula
Definition: A formula which is \(\mathbb Q\)-satisfied by a rational timed state sequence
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1

Smaller0: \(\tau\models\phi\)
Greater0: \(\tau\models_{\mathbb Q}\phi\)
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1
Variables: \(\phi\) a MITL formula,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \), a rational timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem
Smaller to greater: iff
Assuming: \(\tau\) is \(\phi\)-fine
Counterexample: \(\lozenge p\) with \(([0,\sqrt2), \emptyset)(\sqrt2,p)((\sqrt2,\emptyset))\)

Name: The fractional part of \(r\)
Definition: \(r-\lfloor r\rfloor\)
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1
Variables: \(r\in\mathbb R\)
Notation: \(\langle r\rangle\)

Smaller0: \(\tau\sim\tau'\)
Greater0: \(\tau\models\phi\iff\tau'\models\phi\) for each \(\phi\) in MITL
Page: 123
Chapter: The Benefits of Relaxing Punctuality
Section: 4.1
Variables: \(\tau=(\overline s,\overline I)\),
\(\tau'=(\overline s,\overline I')\)
Index: 3
Kind: Lem

Question: \(\tau_\phi\) is
Answer: \(\phi\)-fined timed state sequence equivalent to \(\phi\)
Page: 122
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formulas,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots\), a timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem

Question: \(\tau_\phi\) is
Answer: \(\phi\)-fined timed rational state sequence equivalent to \(\phi\)
Page: 122, 124
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formulas,
\(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots\), a rational timed state sequence satisfying the finite-variability condition
Index: 2
Kind: Lem

Smaller0: \(\phi\) is \(\mathbb Q\)-satisfiable
Greater0: \(\phi\) is satisfiable
Page: 124
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formulas,
Index: 4
Kind: Theo
Smaller to greater: iff

Definition: The formula \(\phi\) where each interval \(I\) is replaced by \(c\cdot I\)
Page: 124
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\) a MITL formulas,
\(c>0\)
Notation: \(\phi_c\)
Index: 1
Kind: Lem

Definition: \((s_{0},cI_0)\to(s_{1},cI_{1})\to\dots \)
Page: 124
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \)
\(c>0\)
Notation: \(\tau_c\)
Index: 1
Kind: Lem

Question: \(\tau_c\models\phi_c\)
Answer: iff \(\tau\models\phi\)
Page: 124
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\tau=(s_{0},I_0)\to(s_{1},I_{1})\to\dots \),
\(\phi\in MITL\)
\(c>0\)
Index: 1
Kind: Lem

Definition: \((\square_{(0,c)}\neg\phi)\land(\lozenge_{(0,c]}\phi)\)
Page: 125
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5
Variables: \(\phi\in MITL\)
Notation: \(\neg\phi\mathcal U_{=c}\phi\)

Definition: The extension of MITL with \(=\) subscript authorized on until operator
Page: 125
Chapter: The Benefits of Relaxing Punctuality
Section: 3.5

Question: it is
Answer: omitted, and jump to next section
Page: 125
Chapter: 2
Section: 4.3
Index: 3
Kind: Theo

Definition: \(\sigma''=(\sigma+t)[\gamma:=0]\)
Page: 129
Section: 3.2
Variables: \(A=(V,V^0,\alpha,X,\beta,E)\) a timed automaton
\((v,\sigma),(v',\sigma ')\in V\times \Sigma\)
Notation: \((v,\sigma)\Rightarrow(v',\sigma ')\)
Definition2: \(\sigma'=\sigma''+t'\)
Conjdef: There exists \(\sigma''\in\Sigma\), and \(t,t'\ge0\) and \(v\xrightarrow\gamma v'\) such that
Definition3: \(\sigma+t''\models\beta(v)\) for each \(t''\in[0,t)\)
Definition4: \(\sigma''+t''\models\beta(v')\) for each \(t''\in(0,t']\)
Definition5: either \(\sigma+t\models\beta(v)\) or \(\sigma''\models\beta(v')\)

Name: A timed automaton
Definition: \(V\) Finite set of locations
Page: 126
Section: 3.1.1
Definition2: Set of initial locations \(V^0\subseteq V\)
Conjdef: The tuple with
Definition3: \(\alpha:V\to 2^{2^P}\)
Definition4: \(X\) A set of clocks
Definition5: \(\beta:V\times X\to2^{\mathbb R^0}\)
Definition6: Set of transitions \(E\subseteq V\times V\times 2^X\)

Name: A transition
Definition: Going from \(v\) to \(v'\) resetting \(\gamma\)
Page: 126
Section: 3.1.1
Variables: \(P\) a set of propositional constraint.
\(A=(V,V^0,\alpha,X,\beta,E)\) a timed automaton,
\(v,v'\in V\),
\(\gamma\subseteq X\)
Denoted by: \(v\xrightarrow\gamma v'\)

Name: A fairness requirement
Typ: A set of locations of \(A\)
Page: 131
Section: 3.1.1
Variables: \(P\) a set of propositional constraint.
Let \(A=(V,V^0,\alpha,X,\beta,E)\) a timed automaton,
Index: 1
Kind: Def

Name: A fairness condition
Definition: A set of fairness requirement
Page: 131
Section: 3.1.1
Variables: \(P\) a set of propositional constraint.
Let \(A=(\mathrm V,V^0,\alpha,X,\beta,E)\) a timed automaton,
Index: 1
Kind: Def
Denoted by: \(\mathcal F\)

Name: A fair timed automaton
Definition: A timed automaton with a fairness condition
Page: 131
Section: 3.1.1
Variables: \(P\) a set of propositional constraint.
Denoted by: \(B\)

Name: A fair run of \(B\)
Definition: A run \(\xrightarrow[\sigma_0]{}(v_0,I_0)\xrightarrow[\sigma_1]{\gamma_1}(v_1,I_1)\dots\) of \(A\) such that for each \(F\in\mathcal F\), there is infinitely many \(v_i\in F\)
Page: 131
Section: 3.4
Variables: \(P\) a set of propositional constraint.
\(A=(\mathrm V,V^0,\alpha,X,\beta,E)\) a timed automaton,
\(B=(A,\mathcal F)\) a fair timed automaton

Name: Something accepted by \(B\)
Definition: A timed state sequence equivalent to a timed state sequence that is generated by a fair run of \(A\)
Page: 131
Section: 3.4
Variables: \(P\) a set of propositional constraint.
\(A=(\mathrm V,V^0,\alpha,X,\beta,E)\) a timed automaton,
\(B=(A,\mathcal F)\) a fair timed automaton

Definition: The set of timed state sequences accepted by \(B\)
Page: 131
Section: 3.4
Variables: \(P\) a set of propositional constraint.
\(A=(\mathrm V,V^0,\alpha,X,\beta,E)\) a timed automaton,
\(B=(A,\mathcal F)\) a fair timed automaton
Notation: \(L(B)\)

Name: todo
Page: 131
Section: 4.1.1
Variables: \(\phi\in\mathrm{MITL}\) in normal form
\(K\) the largest integer constant in \(\phi\), plus one
Let \(N\) the number of subformulas of \(\phi\)

Name: An MITL formula in normal form
Definition: each \(\lozenge_I\psi'\) and \(\square_I\psi'\) have \(l(I)=0\) and left-open
Page: 131
Section: 4.1.1
Definition2: each \(\psi_1\mathcal U\psi_2\) and \(\psi_1\mathcal W\psi_2\) have \(l(I)>0\) and \(r(I)\) finite
Conjdef: An MITL formula in negation normal form
Definition3: \(\square\psi'\) and \(\psi_1\mathcal U\psi_2\) are also accepted

Question: Normal form of \(\psi_1\mathcal U_{I}\psi_2\)
Answer: \(\psi_2^*\lor\psi_1^*\mathcal U_{I\setminus 0}\psi_2^*\)
Page: 131
Section: 4.1.1
Variables: \(\psi_i\in\mathrm{MITL}\)
\(I\) an interval containing 0

Question: Normal form of \(\psi_1\mathcal U_{(a,\infty)}\psi_2\)
Answer: \(\square_{(0,a]}\left(\psi_1^*\land\psi_1^*\mathcal U\psi_2^*\right)\)
Page: 131
Section: 4.1.1
Variables: \(\psi_i\in\mathrm{MITL}\)
Let \(a\in\mathbb R\)

Question: Normal form of \(\psi_1\mathcal U_{[a,\infty)}\psi_2\)
Answer: \(\square_{(0,a)}\psi_1^*\land\square_{(0,a]}(\psi_2^*\lor(\psi_1^*\land\psi_1^*\mathcal U\psi_2^*))\)
Page: 131
Section: 4.1.1
Variables: \(\psi_i\in\mathrm{MITL}\)
Let \(a\in\mathbb R\)

Definition: A modal operator whose interval is \((0,\infty)\)
Page: 121
Section: 2.3.2
Denoted by: Omitting subscript of a modal operator

Definition: A formula, equivalent to \(\psi\), in normal form
Page: 131
Section: 4.1.1
Variables: \(\psi\in\mathrm{MITL}\)
Notation: \(\psi^*\)

Question: Normal form of \(\psi_1\mathcal U_I\psi_2\)
Answer: is \(\diamond _I\psi_2^*\land\psi_1^*\mathcal U\psi_2^*\)
Page: 131
Section: 4.1.1
Variables: \(\psi_i\in\mathrm{MITL}\),
\(I\) an interval such that \(l(I)=0\)

Question: Normal form of \(\psi_1\mathcal W\psi_2\)
Answer: \(\square\psi_1^*\lor\psi_1^*\mathcal U(\psi_1^*\land\psi_2^*)\)
Page: 131
Section: 4.1.1
Variables: \(\psi_i\in\mathrm{MITL}\),

Smaller0: formulas are represented using DAGs
Greater0: linear in the size of \(\psi\)
Page: 131
Section: 4.1.1
Variables: \(\psi\in\mathrm{MITL}\),
Index: 2
Kind: Lem
Prefix Greater: the size of \(\psi^*\) is

Name: A timed state sequence in \(\phi\)-formal form
Definition: A timed state sequence which is \(\phi\)-fine
Page: 132
Section: 4.1.2
Variables: \(\phi\in\mathrm{MITL}\),
Index: 21
Kind: Def
Definition2: and such that all intervals are either singular or open

Definition: \(\tau^t\models\psi\) for each \(t\in I_i\)
Page: 133
Section: 4.1.2
Variables: \(\phi\in\mathrm{MITL}\),
\(\psi\) a subformula of \(\phi\)
\(\tau=(\bar s,\bar I)\)
\(i\in\mathbb N\)
Notation: \(\tau^i\models\psi\)
Assuming: \(\tau\) in normal form

Definition: \(I_i\) is singular
Page: 133
Section: 4.1.2
Variables: \(\tau=(\bar s,\bar I)\)
\(i\in\mathbb N\)
Notation: \(\tau^i\models p_{sing}\)
Definition2: \(i\) even

Smaller0: \(\tau\) in normal form
\(\psi_1,\psi_2\) in normal form
Greater0: there is \(i\in\mathbb N\) such that:
-\(I_1\cap I\ne\emptyset\),
-\(\tau^i\models\psi_2\)
-\(\tau^i\models\psi_1\lor p_{sing}\)
-\(\tau^j\models\psi_1\) for all \(0<j<i\) and
-\(\tau^0\models\psi_1\lor p_{sing}\)
Page: 133
Section: 4.1.2
Variables: \(\psi_1,\psi_2\in\mathrm{MITL}\),
\(I\)
\(\tau=(\bar s,\bar I)\)
\(I\) an interval
Prefix Greater: \(\tau\models\psi_1\mathcal U_I\psi_2\) iff

Name: Timed-constrained unless operator
Definition: \(\neg(\neg\phi_2\mathcal W_I\neg\phi_1)\)
Page: 121
Section: 2.3.3
Variables: \(\phi_1,\phi_2\in\mathrm{MTL}\),
\(I\) an interval
Notation: \(\phi_1\ _I\mathcal W\phi_2\)
Definition2: Either \(\phi_1\) is true throughout the interval \(I\), or there is \(t'>0\) such that \(\phi_2\) is true at time \(t'\) and \(\phi_1\) holds throughout the interval \([t,t']\cap I\)

Name: A witness for \(\psi_1\mathcal U_I\psi_2\) under \(\tau^t\)
Definition: \(I'\) such that \(I'\) intersects \((t+I)\) and
Page: 136
Section: 4.2.2.2
Variables: \(\psi_1,\psi_2\in\mathrm{MTL}\),
\(\tau\) a timed state sequence,
\(t\in\mathbb R_{\ge0}\),
\(I\) a bounded interval with \(l(I)>0\)
Index: 1
Kind: Def
Definition2: and such that  \(\tau^t\models\psi_1\mathcal U_{J-t}\psi_2\) for every nonempty interval \(J\subseteq I\)
Typ: An interval

Name: A witness for \(\psi_1\mathcal W_I\psi_2\) under \(\tau^t\)
Definition: \(I'\) such that \((t+I)\subseteq I'\) and
Page: 136
Section: 4.2.2.2
Variables: \(\psi_1,\psi_2\in\mathrm{MTL}\),
\(\tau\) a timed state sequence,
\(t\in\mathbb R_{\ge0}\),
\(I\) a bounded interval with \(l(I)>0\)
Index: 1
Kind: Def
Definition2: \(\tau^t\models\psi_1\ _{I'-t}\mathcal W\psi_2\)
Typ: An interval

Smaller0: \(t'\in I'\)
Greater0: \(\tau^{t'}\models\psi_2\)
Page: 136
Section: 4.2.2.2
Variables: \(\psi_1,\psi_2\in\mathrm{MTL}\),
\(\tau\) a timed state sequence,
\(t\in\mathbb R_{\ge0}\),
\(I\) a bounded interval with \(l(I)>0\),
\(I'\) a witness for \(\psi_1\mathcal U_I\psi_2\) under \(\tau^t\)
\(t'>0\)
Index: 1
Kind: Def

Smaller0: there is a witnessing interval for \(\psi_1\mathcal U_I\psi_2\) under \(\tau^t\)
Greater0: \(\tau^t\models\psi_1\mathcal U_I\psi_2\)
Page: 136
Section: 4.2.2.2
Variables: \(\psi_1,\psi_2\in\mathrm{MTL}\),
\(\tau\) a timed state sequence,
\(t\in\mathbb R_{\ge0}\),
\(I\) a bounded interval with \(l(I)>0\),
Index: 2
Kind: Lem
Smaller to greater: iff