Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / The Compound Interest in Relaxing Punctuality
Tags: toBinaryRelation autDone clockLocationInitialTransition defToAut fromAlgorithm
On every note of this deck, unless a note says otherwise:
Chapter: The compound interest in relaxing punctality
Chapter: The compound interest in relaxing punctality
Chapter: The compound interest in relaxing punctality

Name: The Minkowski sum of \(t\) and \(R\)
Definition: the set of \(t+r\) with \(r\in R\)
Page: 3
Section: 2
Variables: \(R\subseteq\mathbb T\)
\(t\in\mathbb T\)
Notation: \(t\oplus R\)

Name: The Minkowski sum of \(S\) and \(R\)
Definition: the set of \(s+r\) with \(r\in R\) and \(s\in S\)
Page: 3
Section: 2
Variables: \(R\subseteq\mathbb T\)
\(t\in\mathbb T\)
Notation: \(S\oplus R\)

Page: 3
Definition: The relation from states \((l,v)\) to \((l,v+t)\)
Section: 2
Variables: \(\mathcal A=(\Sigma,X,L,S,F,\Delta)\) a TA
\(t\in\mathbb T\)
Notation: \[\leadsto^t\]

Page: 3
Definition: The relation from states \((l,v)\) to \((l',v[Z\leftarrow 0])\) when \((l,a,\phi,Z,l')\in\Delta\) and \(v\models\phi\)
Section: 2
Variables: \(\mathcal A=(\Sigma,X,L,S,F,\Delta)\) a TA
\(a\in\Sigma\)
Notation: \(\xrightarrow a\)

Name: Deterministic timed automaton
Definition: whose set of initial location is a singleton
Page: 3
Section: 2
Definition2: for each \((l,a,\phi_1,Z_1,l_1)\) and \((l,a,\phi_2,Z_2,l_2)\) in \(\Delta\), \(\phi_1\land\phi_2\) is unsatisfiable
Conjdef: A TA

Name: Timed regular expression
Definition: containing \(\epsilon\)
Page: 3
Section: 2
Definition2: containing \(a\) for \(a\in\Sigma\)
Conjdef: The least set of expressions
Definition3: closed under \(\cup\)
Abbreviation: TRE
Definition4: closed under \(\cdot\)
Definition5: closed under Kleene star
Definition6: closed under \(\phi_I\) for \(\phi\) in this set, and \(I\) an integer-bound interval

Name: The language defined by \(\phi\)
Page: 3
Section: 2
Variables: \(\phi\) a TRE
Notation: \(\mathcal L(\phi)\)

Definition: the set of words \(w\in\mathcal L(\phi)\) whose duration [$]\norm{w}\in I[/$]
Page: 3
Section: 2
Variables: \(\phi\) a TRE,
\(I\) an integer bounded interval
Notation: \(\mathcal L(\phi_I)\)

Name: The duration of \(w\)
Definition: \(\sum t_i\)
Page: 3
Section: 2
Variables: \(w=t_1a_1\dots t_na_n\) a timed-word
Context: Timed word
Notation: [$]\norm{w}[/$]

Name: A pointed word
Definition: A pair \((w,i)\) with \(w\) a timed words and [$]0<i\le\abs{w}+1[/$]
Page: 3
Section: 2

Name: The size of \(\phi\)
Definition: The number of temporal operator of \(\phi\)
Page: 3
Section: 2
Variables: \(\phi\) a MITL formula

Definition: \(\left\lceil{\frac{\text{sup}I}{\text{sup}I-\text{inf}I}}\right\rceil+2\) if \(\text{sup}I<\infty\), \(1\) otherwise
Page: 3
Section: 2
Variables: \(I\) an integer-bounded interval
Notation: \(r(\mathcal U_I)\)

Name: The resolution of \(\psi\)
Definition: the greatest \(r(\mathcal U_I)\) for \(\mathcal U_I\) occurring in \(\psi\)
Page: 3
Section: 2
Variables: \(\psi\) a MITL formula
Context: MITL
Notation: \(r(\psi)\)

Question: A timed automaton accepting \(\mathcal L(\phi)\) has
Answer: number of clocks is the depth of \(\phi\)
Page: 3
Section: 2
Variables: \(\phi\) a TRE
Answer2: number of location is the size, plus one.
Index: 1
Kind: Index

Question: A timed automaton accepting \(\mathcal L(\phi)\) has
Answer: [$]2r(\phi)\abs{\phi}[/$] clocks
Page: 3
Section: 2
Variables: \(\phi\) a MITL ormula
Answer2: [$]2^{8r(\phi)\abs{\phi}+1}[/$] clocks
Kind: Theo

Name: Metric interval regular expressions
Definition: TRE of depth 1, devoid of singular timing intervals
Page: 4
Section: 3
Abbreviation: MIRE

Name: Metric interval automaton
Definition: with a single clock \(x\)
Page: 5
Section: 3
Definition2: for each transition \((\ell,a,\phi,Z,\ell')\), either \(\phi=\top\) and \(Z=\emptyset\) or \(\phi\) is \(x\in I\) and \(Z=\{x\}\)
Conjdef: A timed automaton
Abbreviation: MIA

Page: 5
Implementation: Transform \((\ell,\gamma,x\in I,\{x\},\ell')\) into \((\ell,(\gamma)_I,\top,\emptyset,\ell')\). Then apply the standard algorithm to transform automata into regular expressions
Section: 3
Chapter: The compound interest in relaxing punctality
Effect: A Metric Interval Regular Expression accepting the same language than \(\mathcal A\)
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton

Question: Example of language not expressible using a single clock
Answer: \(\square(a\to \lozenge_{[1,2]}b)\)
Page: 5
Section: 3

Question: Example of untimed language not expressible in MITL
Answer: \((a^2)^*\)
Page: 5
Section: 3

Question: Example of language expressed in MIRE and not expressible in MITL
Answer: \(a\cdot((a^+)_{[1,2]})^+\)
Page: 5
Section: 3

Question: \(\mathcal A_\epsilon\)
Answer: An automaton with a single location, final and initial, no transition
Page: 6
Section: 4
Context: MIRE to MIA

Question: \(\mathcal A_a\)
Answer: An automaton with a initial and a final location, and a label from initial to final labelled by \(a\)
Page: 6
Section: 4
Variables: \(a\in\Sigma\)
Context: MIRE to MIA

Question: \(\mathcal A_{\phi\cup\psi}\)
Answer: The union of \(\mathcal A_{\phi}\) and of \(\mathcal A_{\psi}\), with the initial states merged
Page: 6
Section: 4
Variables: \(\phi,\psi\) MIREs
Context: MIRE to MIA

Question: \(\mathcal A_{\phi\cdot\psi}\)
Answer: \((\Sigma,\{x\},L_\phi\cup L_\psi\setminus\{\ell_\phi\}, S_{\phi\cdot\psi},\{\ell_\psi\},\Delta_{\phi\cdot\psi})\) with:
-\(S_\phi\) if \(l_\phi\not\in S_\phi\), \(S_\phi\cup S_\psi\setminus\{\ell_\phi\}\) otherwise
-\(\Delta_{\phi\cdot\psi}\) is \(\Delta_\phi\cup\Delta_\psi\) where the \((\ell,a,\phi,Z,\ell_\phi)\) is replaced by \((\ell,a,\phi,Z,\ell')\) for all \(\ell'\in S_\phi\)
Page: 6
Section: 4
Variables: \(\phi,\psi\) MIREs
Context: MIRE to MIA

Question: \(\mathcal A_{\phi^*}\)
Answer: \(\mathcal A_{\epsilon\cup\phi^+}\)
Page: 6
Section: 4
Variables: \(\phi,\psi\) MIREs
Context: MIRE to MIA

Question: \(\mathcal A_{\phi^+}\)
Answer: \((\Sigma,\{x\},L_\phi,S_\phi,\ell_\phi,\Delta_\phi\cup\{(\ell,a,\phi,Z,\ell')\mid(\ell,a,\phi,Z,\ell_\phi)\in\Delta_\phi,\ell'\in S_\phi\})\)
Page: 6
Section: 4
Variables: \(\phi,\psi\) MIREs
Context: MIRE to MIA

Question: \(\mathcal A_{\gamma_I}\)
Answer: \((\Sigma,\{x\},L_\gamma,S_{\gamma_I},\ell_\gamma,\{(\ell,a,x\in I,\{x\},\ell_\gamma)\mid(\ell,a,\top,\emptyset,\ell_\phi)\in\Delta_\gamma\})\) with:
-\(S_\gamma\) if \(0\in I\), \(S_{\gamma}\setminus \{\ell_\gamma\}\) otherwise
Page: 6
Section: 4
Variables: \(\phi,\psi\) MIREs
Context: MIRE to MIA

Definition: The MIA \((\Sigma,\{x\},L_\phi,S_\phi,\{\ell_\phi\},\Delta_\phi)\)
Page: 6
Section: 4
Variables: \(\phi\) MIREs
Context: MIRE to MIA
Notation: \(\mathcal A_\phi\)

Name: An interval state of \(\mathcal A\)
Definition: \((\ell,J)\) with \(\ell\) a location and \(J\) an interval
Page: 7
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Intuition: the set of \((\ell,t)\) with \(t\in J\)

Name: A configuration
Definition: A set of interval states
Page: 7
Section: 4
Variables: \(\mathcal A\) a metric interval automaton

Page: 7
Definition: the relation from \(C\) to \(\{(\ell,t\oplus J)\mid (\ell,J)\in C\}\)
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Notation: \(\leadsto ^t\)
Context: MIA configurations

Page: 7
Definition: \((\ell,J)\) to \((\ell',J)\) where \((\ell,a,\phi,\emptyset,\ell')\in\Delta\) with \(t\models\phi\) for some \(t\in J\)
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Notation: \(\xrightarrow a\)
Context: MIA configurations
Definition2: \((\ell,J)\) to \((\ell',\{0\})\) where \((\ell,a,\top,\{x\},\ell')\in\Delta\) with \(t\models\phi\) for some \(t\in J\)
Symmetry: the relation containing

Page: 7
Definition: the relation from \(C\) to \(\{(\ell',t')\mid\exists (\ell,J)\in C, (\ell,J)\xrightarrow a(\ell',J')\}\)
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Notation: \(\xrightarrow a\)
Context: MIA configurations

Name: The parallel run of \(\mathcal A\) over \(w\)
Definition: A sequence of transition \((\ell,[0,0])\leadsto ^{t_1}C'_0\xrightarrow{a_1}\dots\leadsto^{t_n}C'_{n-1}\xrightarrow {a_n}C_n\) for \(\ell\) initial
Page: 7
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(w=t_1a_1\dots t_na_n\) a timed word
Context: MIA configurations

Smaller0: there exists a run of \(\mathcal A\) over \(w\) finishing in \(\ell\)
Greater0: the final configuration of the parallel run of \(\mathcal A\) over \(w\) feature \(\ell\)
Page: 7
Chapter: The compound interest in relaxing punctality
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(w=t_1a_1\dots t_na_n\) a timed word
\(\ell\) a location
Index: 1
Kind: Lem
Smaller to greater: iff
Context: MIA configurations

Definition: \(C\setminus\{(\ell,I),(\ell,J)\}=D\setminus\{(\ell,\text{ch}(I\cup J))\}\) for some \((\ell,I)\ne(\ell,J)\in C\), \((\ell,\text{ch}(I\cup J))\in D\), with \(\text{inf} J-\text{sup} I\) \(\text{inf} I-\text{sup} J\) less than the length of the longest interval of \(\mathcal A\), or \(\text{sup}(I\cup J)\) greater than some finite interval lower bound.
Page: 7
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(C,D\) configurations
Notation: \(C\prec D\)

Definition: \(D\) is maximal relative to \(\prec\) such that \(C\prec^* D\)
Page: 7
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(C,D\) configurations
Notation: \(C\dashrightarrow^\prec D\)

Definition: The transitive closure of \(\prec\)
Page: 8
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Notation: \(\prec^*\)

Name: The \(\prec\)-parallel run of \(\mathcal A\) over \(w\)
Definition: A sequence of transition \((\ell,[0,0])\leadsto ^{t_1}C'_0\dashrightarrow^\prec C_0''\xrightarrow{a_1}\dots\leadsto^{t_n}C'_{n-1}\xrightarrow {a_n}C_n\dashrightarrow^\prec C_n''\) for \(\ell\) initial
Page: 8
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(w=t_1a_1\dots t_na_n\) a timed word

Smaller0: the set of locations that appear in final configurations of the parallel run
Greater0: the set of locations that appear in final configurations of the \(\prec\)-parallel run
Page: 8
Chapter: The compound interest in relaxing punctality
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
\(w=t_1a_1\dots t_na_n\) a timed word
Smaller to greater: equals

Name: The resolution of \(\mathcal A\)
Definition: For \(c\) the least bound of finite interval, \(d\) the greatest length of interval, \(\left\lfloor\frac cd\right\rfloor+2\) if \(d<@\infty\), \(1\) otherwise
Page: 8
Section: 4
Variables: \(\mathcal A\) a metric interval automaton
Notation: \(r(\mathcal A)\)

Question: in \(C\dashrightarrow^\prec D\), [$]\abs{D}[/$] is
Answer: at most [$]\abs{L}r(\mathcal A)[/$]
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(C\) a configuration of \(\mathcal A\)

Definition: \(\bigwedge_{\ell yy'\in P,(\ell,a,\phi,Z,\ell')\in E}\phi[yy']\land\bigwedge_{\ell yy'\in P,(\ell,a,\phi,Z,\ell')\in\Delta(P,a)\setminus E}\neg\phi[yy']\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(P\in L',Q\),
\(a\in\Sigma\),
\(E\subseteq\Delta\),
Notation: \(\theta(P,E)\)
Intuition: Constraint ensuring that \(E\) is exactly the set of edges of \(\mathcal A\) that can be taken from \(P\),

Definition: \(\{\ell'yy'\mid \ell yy'\in P,(\ell,a,\top,\emptyset,\ell')\in E\}\cup\{\ell'y_0y'_0\mid (\ell,a,\phi,\{x\},\ell')\in E\}\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(P\in L',Q\),
\(a\in\Sigma\),
\(E\subseteq\Delta\),
Notation: \(R(P,E)\)
Intuition: Configuration reached when taking the edges \(E\) from \(P\)

Definition: \[\begin{array}{ll}((y_i-y'_{j'}<c\land y_j-y'_{i'}<c)\lor (y_i>d\land y_j>d))&\land\\(y_i>y_k\lor(y_i=y_k\land i\le k))&\land\\((y_j>y_k\lor y_j=x_k)\land j\le k)&\land\\(y'_{i'}<y'_{k'}\lor(y'_{i'}=y'_{k'}\land i'\le k'))&\land\\(y'_{j'}\le y'_{k'}\lor (y'_{j'}=y'_{k'}\land j'\le k'))& \end{array}\]
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(R,Q\in L'_0\),
[$]i'jj'\in\{0,\dots,\abs{L}r(\mathcal A)\}[/$]
\(k\in\{i,j\}\)
\(k\in\{i',j'\}\)
Notation: \(\mu_{ii'jj'kk'}\)
Intuition: ensures that \(\ell y_iy'_{i'}\) and \(\ell y_jy'_{j'}\) should be merged to \(\ell y_ky'_{k'}\)

Definition: if both \(y_0,y'_0\in Q\), then \(\{y_i,y'_{i'}\}\) for \(i,i'\ge 1\) least indices such that \(y_i,y'_{i'}\not\in Q\)
Page: 9
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(Q\in L'_0\),
Notation: \(Z_Q\)
Definition2: if \(y_0\in Q\), \(y'_0\not\in Q\), then \(y_i\) for \(i\) the least index such that \(y_i\not\in Q\)
Conjdef: Either
Definition3: otherwise, if \(y_0,x'_0\not\in Q\), then \(\emptyset\)

Definition: disjunction over well formed chains of merges \(i_1i'_1j_1j'_1k_1k'_1,\dots,i_hi'_hj_hj'_hk_hk'_h\) from \(R\) to \(Q\) of the \(\mu_{i_ni'_nj_nj'_nk_nk'_n}\)'s
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(R,Q\in L'_0\),
Notation: \(\lambda_\prec(R,Q)\)
Definition2: the conjunction of \(\neg\mu_{ii'jj'kk'}\) of all possible merges in \(Q\)
Conjdef: The conjunction of
Intuition: Constraint ensuring that \(Q\) approximates the configuration reached

Definition: The configuration \(Q\), in which \(y_0\) (resp. \(y'_0\)), if present in \(Q\), are replaced by \(y_i\) (resp. \(y'_{i'}\)), with \(i\) (resp. \(i'\)) the least positive integer such that \(y_i\not\in Q\) (resp. \(y'_i\not\in Q\))
Page: 9
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
\(Q\in L'_0\),
Notation: \(\overline Q\)

Page: 8, 9
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton
Section: 4
Chapter: The compound interest in relaxing punctality
Transitions: \((P,a,\theta(P,E)\land\lambda_\prec(R(P,E),Q)Z_Q,\overline Q)\) for \(P\in L'\), \(a\in\Sigma\), \(Q\in L'_0\), \(E\subseteq \Delta(P,a)\)
Initial: Initial location \(S\times\{y_1\}\times\{y'_1\}\)
Name: The deterministic timed automaton equivalent to \(\mathcal A\)
Final: The deterministic timed automaton \(\mathcal A'(\Sigma,X',L',S',F',\Delta')\)
Locations: locations \(2^{L\times Y\times Y'}\)
Clock number: clocks, the union of [$]Y=\{y_1,\dots, y_{\abs{L}r(\mathcal A)}\}[/$] and of [$]Y=\{y_1,\dots, y'_{\abs{L}r(\mathcal A)}\}[/$]

Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
\(y\in Y\),
\(y'\in Y'\)
\(v\) a valuation
Context: Deterministic version of \(\mathcal A\)
Notation: \(yy'\)
Intuition: the interval \([v(y),v(y')\)

Definition: The set of \((\ell,[v(y),v(y')])\mid \ell yy'\in Q\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
\(Q\in L'\) a location of the determinisation of \(\mathcal A\)
Context: Deterministic version of \(\mathcal A\)
Notation: \(v(Q)\)

Definition: \(\phi\) where lower bound comparison of \(x\) are replaced by \(y\), and higher bound by \(y'\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
\(y\in Y\)
\(y'\in Y'\)
\(\phi\in\Phi(\{x\})\)
Context: Deterministic version of \(\mathcal A\)
Notation: \(\phi[yy']\)

Smaller0: \(v\models\phi[yy']\)
Greater0: there exists \(t\in[v(y),v(y')]\) such that \(t\models\phi\)
Page: 8
Chapter: The compound interest in relaxing punctality
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
\(y\in Y\)
\(y'\in Y'\)
\(\phi\in\Phi(\{x\})\)
\(v\) a valuation
Smaller to greater: iff
Context: Deterministic version of \(\mathcal A\)

Definition: The set of edges \((\ell,a,\phi,Z,\ell')\in\Delta\) with \(\ell\in P\).
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
\(P\in L'\)
\(a\in\Sigma\)
Notation: \(\Delta(P,a)\)

Definition: \(Y\cup\{y_0\}\), \(Y'\cup\{y_0\}\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
Context: Determinisation of MIA
Notation: \(Y_0\), \(Y'_0\)

Definition: \(2^{L\times Y_0\times Y'_0}\)
Page: 8
Section: 4
Variables: \(\mathcal A=(\Sigma,\{x\},L,S,F,\Delta)\) a Metric interval automaton,
Context: Determinisation of MIA
Notation: \(L'_0\)