Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Checking timed and hybrid properties: theory and applications

Name: Back to operator
Context: MITL
Notation: \(\mathcal B\)

Name: \(w\) positively determines \(\phi\)
Definition: For each infinite completion \(w'\) of \(\phi\), \(w'\models\phi\)
Page: 28
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula

Name: \(w\) negatively determines \(\phi\)
Definition: For each infinite completion \(w'\) of \(\phi\), \(w'\not\models\phi\)
Page: 28
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula

Name: \(w\) is undecided for \(\phi\)
Definition: \(w\) neither positively nor negatively determines \(\phi\)
Page: 28
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula

Definition: the set of infinite words \(w'\) such that \(w\cdot w'\models\phi\)
Page: 29
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula
Notation: \(w\setminus\phi\)
Intuition: Left quotient of the semantic of \(\phi\) by \(w\)

Definition: \((w,t)\setminus\circ\phi\)
Page: 29
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula
[$]t\le\abs{w}[/$]
Notation: \((w,t)\setminus\circ^s\phi\)
Definition2: [$]t=\abs{w}[/$]
Conjdef: Either

Definition: \((w,t)\setminus\circ\phi\)
Page: 29
Chapter: 2
Variables: \(w\) a finite word
\(\phi\) a LTL formula
[$]t\le\abs{w}[/$]
Notation: \((w,t)\setminus\circ^w\phi\)
Definition2: [$]t<\abs{w}[/$]
Conjdef: Both

Name: Weak next-time operator
Page: 29
Chapter: 2
Context: LTL
Notation: \(\circ^w\)

Name: Strong next-time operator
Page: 29
Chapter: 2
Context: LTL
Notation: \(\bigcirc^s\)

Name: The characteristic function of \(\phi\)
Definition: The function associating to each word \(w\), at each time \(t\), the transducer outputs \(1\) iff \((w,t)\models\phi\)
Page: 29
Chapter: 2
Variables: \(p_1,\dots,p_n\) a set of propositional variables
\(\phi\) a LTL formula
Context: LTL
Notation: \(\Xi^\phi\)

Name: A temporal tester for \(\phi\)
Definition: A transducer \(\mathbb B^n\to\mathbb A\) which implements the characteristic function \(\Xi^\phi\)
Page: 29
Chapter: 2
Variables: \(p_1,\dots,p_n\) a set of propositional variables
\(\phi\) a LTL formula
Context: LTL
Intuition: An automaton guessing output, and checking them later
Denoted by: \(T_\phi\)

Name: A sequential function
Definition: A function mapping sequence to sequence
Context: LTL

Name: A causal sequential function
Definition: A sequential function \(f:A^\omega\to B^\omega\) such that for each \(u\in A^*,v,v'\in B^*\) with [$]\abs{u}=\abs{v}=\abs{v'}[/$], and every \(\alpha\in A^\omega\) \(\beta\in B^\omega\), \(f(u\cdot\alpha)=v\cdot\beta\) and \(f(u\cdot\alpha')=v'\cdot\beta'\) implies \(v=v'\)
Page: 34
Chapter: 2
Section: 3.2
Variables: \(A,B\) alphabets
Context: LTL
Intuition: The \(n\)-th output is determined by the \(n\)-first letters

Name: An acausal sequential function
Definition: A sequence function which is not causal
Page: 34
Chapter: 2
Section: 3.2
Variables: \(A,B\) alphabets
Context: LTL

Name: A signal
Definition: A function \(\mathbb T\to D\) with \(\mathbb T\) a time domain
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
Context: Model checking

Name: A punctual signal
Definition: A signal whose time domain is \(\{0\}\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
Context: Signals
Denoted by: \(\dot w\)

Name: An open signal segment
Definition: A signal whose time domain is \((0,r)\) for some \(r>0\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
Context: Signals
Denoted by: \((w)_r\)

Name: A time domain
Definition: Either \(\mathbb R_{\ge0}\) or \((0,r)\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
Context: Signals

Name: A finite signal
Definition: The concatenation of a punctual signal and an open signal segment
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
Context: Signals
Denoted by: \(w\)

Definition: The finite signal sending \(t\) to \(w_1(t)\) if \(t<r_1\), else to \(w_2(r_1+t)\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
\(r_1,r_2>0\)
\(w_i:\mathbb [0,r_i)\to D\) signals
Context: Signals
Notation: \(w_1\cdot w_2\)

Name: A point-segment partition of \(\mathbb T\)
Definition: An alternating sequence of adjacent points and open interval of the form \(\{t_0\},(t_0,t_1),\{t_1\},\dots\) with \(_0=0\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
\(\mathbb T\) a time domain
Context: Signals
Denoted by: \(J\)

Definition: \(r_i=t_{i+1}-t_{i}\)
Page: 39
Chapter: 3
Section: 1
Variables: \(D\) a domain
\(\mathbb T\) a time domain
\(J\) a point-segment partition of \(\mathbb T\)
Context: Signals
Notation: \(w=\dot w_0\cdot(w_0)_{r_0}\cdot \dot w_1\dots\)
Definition2: \(\dot w_i\) as \(w(t_i)\)
Conjdef: Introduce the variables
Definition3: \((w_i)_{r_i}\) as [$]\defFun{(0,r_i)}{D}{t}{w(t_i+t)}[/$]

Name: An interval splitting of \((t_i,t_{i+1})\)
Definition: A partition \((t_i,t'),{t'},(t',t_{i+1})\)
Page: 39
Chapter: 3
Section: 1
Variables: \((t_i,t_{i+1})\) an interval
Context: Signals

Name: \(J'\) is a refinement of \(J\)
Definition: \(J'\) can be obtained by a finite number of interval splitting of \(J\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(J,J'\) a time-segment partition of \(\mathbb T\)
Context: Signals
Notation: \(J'\prec J\)

Name: \(J\) is compatible with \(w\)
Definition: \(w\) is constant on each open interval of \(J\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(J\) a time-segment partition of \(\mathbb T\)
\(w:\mathbb T\to D\)
Context: Signals

Name: The left limit of \(w\) at \(t\)
Definition: \(\lim_{r\to t^+}w[r]\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
\(t\in\mathbb T\)
Context: Signals
Notation: \(w[\rightarrow t]\)

Name: The right limit of \(w\) at \(t\)
Definition: \(\lim_{r\to t^-}w[r]\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
\(t\in\mathbb T\)
Context: Signals
Notation: \(w[t\leftarrow]\)

Name: A left singular point
Definition: A point \(t\) such that \(w[\rightarrow t]\ne w(t)\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signals

Name: A right singular point
Definition: A point \(t\) such that \(w[t\leftarrow]\ne w(t)\)
Page: 39
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signals
Kind: right

Name: A singular point
Definition: A point \(t\) which is either left-singular or right-singular
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signals
Kind: right

Name: A stationnary point
Definition: A point which is not singular
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signals
Kind: right

Definition: The sequence of singular points in \(w\)
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signals
Notation: \(\mathcal J(w)\)
Kind: right
Denoted by: \(t_0,t_1,\dots\)

Name: A well behaving signal
Definition: A signal \(w:\mathbb T\to D\) such that \(\mathcal J(w)\) is either finite or countable and diverging
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
Context: Signals
Kind: right

Name: The canonical time partition of \(w\)
Definition: \(\{t_0\},(t_0,t_1),\{t_1\},\dots\) where \(\mathcal J(w)=t_0,t_1,\dots\)
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain\(w:\mathbb T\to D\)
Context: Signals
Notation: \(J_w\)
Kind: right

Definition: \(r_i=t_{i+1}-t_i\)
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain\(w:\mathbb T\to D\)
Context: Signals
Notation: \(\dot\sigma_0\cdot\sigma_0^{r_0}\cdot\dot\sigma_1\dots\)
Kind: right
Definition2: \(\dot\sigma_i=w(t_i)\)
Conjdef: Let \(\mathcal J(w)=t_0,t_1,\dots\). Then introduce
Definition3: \(\sigma_i^{r_i}\) the unique value of \(w\) during \((t_i,t_{i+1})\)

Definition: Similar to \(\dot\sigma_0\cdot\sigma_0^{r_0}\cdot\dot\sigma_1\dots\) without singular states
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain\(w:\mathbb T\to D\)
Context: Signals
Notation: \(\sigma_0^{r_0}\cdot\sigma_1^{r_1}\dots\)
Kind: right

Definition: [$]\defFun{\mathbb T}{\mathbb B^2}{t}{(w_p[t],w_q[t])}[/$]
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain\(w_p,w_q:\mathbb T\to \mathbb B\)
Context: Signals
Notation: \(w_p\parallel w_q\)
Kind: right
Denoted by: \(w_{pq}\)

Name: Well behaved signals
Page: 40
Section: 1
Chapter: 3
Variables: \(\mathbb T\) a time domain
\(w_p,w_q:\mathbb T\to \mathbb B\)
Kind: right
Under: pairing
Under2: Projection
Under3: Boolean operations
Under4: \(w_{pq}\)
Condition4: [$]\defFun{\mathbb T}{\mathbb B^2}{t}{(w_p[t],w_q[t])}[/$]

Question: The left bound of \(A\oplus B\) is
Answer: closed iff both the left bonuds of \(A\) and \(B\) are closed
Page: 40
Chapter: 3
Section: 1
Variables: \(A,B\) intervals
Context: Minkowski sum
Kind: right

Definition: [$]\defFun{\mathbb T}{D\cup\{\bot\}}{t}{\begin{array}{l}w[t]\text{ if }t<d\\ \bot\text{ otherwise}\end{array}}[/$]
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
\(d\in\mathbb T\)
Notation: \(\langle w\rangle_d\)

Definition: The value \(w[t]\) when \(d\not\in\mathbb T\)
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
Context: Signal automata
Notation: \(\bot\)

Definition: [$]\defFun{\mathbb T\ominus d}{D}{t}{w[t-d]}[/$]
Page: 40
Chapter: 3
Section: 1
Variables: \(\mathbb T\) a time domain
\(w:\mathbb T\to D\)
\(d\in\mathbb D\)
Context: Signal automata
Notation: \(d\setminus w\)
Index: Removing the \(d\) first time units from \(w\)

Question: How to rewrite \(\phi_1\mathcal U_{\mid a,b\mid}\phi_2\) using simpler formulas
Answer: \(\square_{(0,a\mid}\phi_1\land_{(0,a\mid}(\phi_1\mathcal U\phi_2)\land_{\mid a,b\mid}\phi_2\)
Page: 44
Chapter: 3
Section: 21
Variables: \(\phi_1,\phi_2\) MITL formulas
\(|a,b|\) a finite interval
Context: Signal automata

Question: How to rewrite \(\phi_1\mathcal U_{\mid a,\infty)}\phi_2\) using simpler formulas
Answer: \(\square_{(0,a\mid}\phi_1\land_{(0,a\mid}(\phi_1\mathcal U\phi_2)
Page: 44
Chapter: 3
Section: 21
Variables: \(\phi_1,\phi_2\) MITL formulas
\(|a,\infty)\) an interval
Context: Signal automata

Question: What can be said about the characteristic function of \(\diamond_{\mid a,b\mid}\phi\) ? (i.e. \(\{t\in\mathbb T\mid w,t\models\diamond_{\mid a,b\mid}\phi\}\)
Answer: Each time it becomes true, it stays true for at least \(b-a\) time units
Page: 29
Chapter: 3
Section: 2.1
Variables: \(w\) an arbitrary signal
\(\phi\) a MITL formula
\(\mid a,b\mid\) an interval

Name: A MITL formula of uniform bounded variablility
Definition: A formula \(\phi\) such that, for each signal \(w\), the delay between two occurrences where its characteristic function becomes true is bouded by below
Page: 29
Chapter: 3
Section: 2.1

Question: A normal form of MITL over signal is
Answer: temporal operators \(\mathcal U\), \(\diamond_{(0,a)}\) and finally \(\diamond_a\) over formula whose characteristic functions is of uniform bounded variability
Page: 45
Chapter: 3
Section: 2.1

Name: Rise
Definition: \(\uparrow\)
Page: 45
Chapter: 3
Section: 2.1
Context: MITL

Name: Fall
Definition: \(\downarrow\)
Page: 45
Chapter: 3
Section: 2.1
Context: MITL

Name: Falling \(p\)
Definition: \((\neg p\land(p\mathcal S\top))\lor(p\land(\neg p\mathcal U\top))\)
Page: 45
Chapter: 3
Section: 2.1
Variables: \(p\) in MITL
Context: MITL
Notation: \(\downarrow p\)

Name: A strong operator
Definition: A time operators \(O\) such that, in order for \((w,t)\models O_{I}\) to hold, even if \(t+I\) is not included in the domain of the signal, the property required by \(O\) should still be satisfied
Page: 45
Chapter: 3
Section: 2.2
Context: MITL over finite signal
Example: \(\diamond_Ip\): \(p\) must holds during interval \(I\). If \(t+I\) is not in the domain of definition, then the run is rejected

Name: A weak operator
Definition: A time operators \(O\) such that, in order for \((w,t)\models O_{I}\) to hold, even if \(t+I\) is not included in the domain of the signal, the property is assumed to hold
Page: 45
Chapter: 3
Section: 2.2
Context: MITL over finite signal
Example: \(\square p\): If \(t+I\) is not in the domain of definition, then the run is accepted

Name: A left-continuous signal
Definition: A signal \(\gamma\) such that, for each \(t\), \(\gamma(t)=\gamma[\rightarrow t]\)
Page: 47
Chapter: 3
Section: 2.3
Context: MITL

Name: A right-continuous signal
Definition: A signal \(\gamma\) such that, for each \(t\), \(\gamma(t)=\gamma[\leftarrow t]\)
Page: 47
Chapter: 3
Section: 2.3
Context: MITL

Name: A left/right-continuous formula
Definition: A formula such that the signal \(\gamma\) of its characteristic function is left/right-continuous
Page: 47
Chapter: 3
Section: 2.3
Context: MITL

Name: A left-continuous operator
Definition: An operator \(O\) such that, each formula with principal operator \(O\) is left continuous
Page: 47
Chapter: 3
Section: 2.3
Context: MITL
Index: 4
Kind: Lem
Example: \(\mathcal S\)

Name: A right-continuous operator
Definition: An operator \(O\) such that, each formula with principal operator \(O\) is right continuous
Page: 47
Chapter: 3
Section: 2.3
Context: MITL
Index: 4
Kind: Lem
Example: \(\mathcal U\)

Page: 55
Implementation: Recursivly, bottom-up, compute the formula output using the direct subformula, thanks to function COMBINE
Section: 1
Chapter: 4
Name: Offline marking
Returns: for each subformula \(\psi\) of \(\phi\), computes the characteristic function \(u_\psi\) of \(\psi\) on \(w\)
Input: A signal \(w\) of length \(r\) over \(n\) Boolean formula
A MITL formula \(\phi\)

Page: 55
Implementation: Refine the partition as the union of the partition of \(u_{\psi_1}\) and of \(u_{\psi_2}\), then on each interval \(I\) assign the disjunction of \(u_{\psi_1}\lor u_{\psi_2}\)
Section: 1
Chapter: 4
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
\(\phi=\psi_1\lor\psi_2\) a MITL formula
Name: \(\mathrm{Combine}(\neg,u_{\neg\psi_1},u_{\neg\psi_2})\)

Page: 55
Implementation: Refine the partition as the union of the partition of \(u_{\psi_1}\) and of \(u_{\psi_2}\). At time 0, set the output to false. Then compute using rules for \(\mathcal S\), recursively on the time interval
Section: 1
Chapter: 4
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
\(\phi=\psi_1\mathcal S\psi_2\) a MITL formula
Name: \(\mathrm{Combine}(\mathcal S,u_{\neg\psi_1},u_{\neg\psi_2})\)

Page: 55
Implementation: Refine the partition as the union of the partition of \(u_{\psi_1}\) and of \(u_{\psi_2}\). At last time, set the output to false. Then compute using rules for \(\mathcal S\), recursively on the time interval
Section: 1
Chapter: 4
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
\(\phi=\psi_1\mathcal U\psi_2\) a MITL formula
Name: \(\mathrm{Combine}(\mathcal U,u_{\neg\psi_1},u_{\neg\psi_2})\)

Page: 59
Implementation: Compute the interval \(\mathcal I_w\) covering of \(\psi\). For each \(I^+\in\mathcal I^+_w\), compute \(I^+\ominus I\cap[0,r)\). This is the set of times where \(\lozenge_I\psi\) holds.
Section: 1
Chapter: 4
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
\(\phi=\lozenge_I\psi_1\) a MITL formula
Name: \(\mathrm{Combine}(\lozenge_I,u_{\neg\psi_1},u_{\neg\psi_2})\)

Page: 59
Implementation: Compute the interval \(\mathcal I_w\) covering of \(\psi\). For each \(I^+\in\mathcal I^+_w\), compute \(I^+\oplus I\cap[0,r)\). This is the set of times where \(\phi\) holds.
Section: 1
Chapter: 4
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
\(\phi=\lozenge_I\psi_1\) a MITL formula
Name: \(\mathrm{Combine}(\) \(_I,u_{\neg\psi_1},u_{\neg\psi_2})\)

Name: An interval covering of \([0,r)\)
Definition: A partition of \([0,r)\) by intervals
Page: 59
Chapter: 4
Section: 1.3
Variables: \(r>0\)
Denoted by: \(I_0,\dots,I_k\)

Name: An interval covering consistent with \(w\)
Definition: An interval covering \(\mathcal I\) of \([0,r)\) such that \(w\) is constant on each intervals
Page: 59
Chapter: 4
Section: 1.3
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables

Definition: The minimal interval covering consistent with \(w\)
Page: 59
Chapter: 4
Section: 1.3
Variables: \(w\) a signal of length \(r\) over \(n\) Boolean variables
Notation: \(\mathcal I_w\)

Definition: The set of interval \(I\in\mathcal I_w\) such that \(w[t]=1\) for \(t\in I\)
Page: 59
Chapter: 4
Section: 1.3
Variables: \(w\) a Boolean signal of length \(r\)
Notation: \(\mathcal I^+_w\)

Definition: The set of interval \(I\in\mathcal I_w\) such that \(w[t]=0\) for \(t\in I\)
Page: 59
Chapter: 4
Section: 1.3
Variables: \(w\) a Boolean signal of length \(r\)
Notation: \(\mathcal I^-_w\)

Definition: The signal \(w:\mathbb T\to\mathbb B^m\) satisfying for every \(i\) and for every \(t\), \(w_i[t]=\mu_i(x_1,\dots,x_n)\)
Page: 65
Chapter: 5
Section: 1
Variables: \(\mathbb T\) the time
\(X\subseteq\mathbb R^n\)
\(M=\{\mu_1,\dots,\mu_m\}\) a set of predicates over \(X\)
\(\xi:\mathbb T\to X\)
Notation: The \(M\)-Booleanization of \(\xi\)
Kind: Def

Name: A STL-term
Definition: A constant
Page: 65
Chapter: 5
Section: 1
Kind: Def
Definition2: A real-valued variable \(x\)
Conjdef: Either
Definition3: A function \(f(t_1,\dots,t_n)\) applied to terms

Name: A STL-predicate
Definition: \(t\sim c\) with \(t\) a STL-term, \(c\) a constant, and \(\sim\) being \(=,\le,\ge,<\) or \(>\)
Page: 65
Chapter: 5
Section: 1
Kind: Def

Name: A STL-formula
Definition: A proposition \(p\)
Page: 66
Chapter: 5
Section: 1
Kind: Def
Definition2: \(E\sim c\) a STL-predicate
Conjdef: Either
Definition3: \(\neg\phi\), \(\phi_1\lor\phi_2\)
Definition4: \(\phi_1\mathcal U_I\phi_2\)
Definition5: \(\phi_1\mathcal S_I\phi_2\)