Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Timed-Automata-Based Verification of MITL over Signals
Tags: autDone defToAut
On every note of this deck, unless a note says otherwise:
Chapter: Timed-automata-based verification of MITL over Signals

Name: A signal
Definition: A function \(\mathbb R_{\ge0}\to\mathrm{AP}\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
Denoted by: \(\gamma\)

Name: A finitely variable signal
Definition: A signal \(\gamma\) such that, for each bounded interval \(I\), \(\gamma\) a finite number of discontinuity in \(I\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates

Name: A state sequence over \(2^{\mathrm {AP}}\)
Definition: A sequence \((\sigma_i)_{i\in\mathbb N}\) with \(\sigma_i\in 2^{\mathrm{AP}}\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
Denoted by: \(\overline\sigma\)

Name: A bipartite interval sequence
Definition: An interval sequence \(\overline I=(I_i)_{i\in\mathbb N}\) such that \(I_i\) is singular iff \(i\) is even
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates

Name: A timed state sequence over \(2^{\mathrm{AP}}\)
Definition: \(\overline S\) a state sequence over \(2^{\mathrm{AP}}\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
Definition2: \(\overline I\) an interval sequence
Conjdef: A pair \((\overline\sigma,\overline I)\) with
Denoted by: \(\kappa\)

Definition: \(\sigma_i\) such that \(t\in I_i\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\kappa=(\overline\sigma,\overline I)\) a timed state sequence
\(t\ge 0\)
Notation: \(\kappa(t)\)

Definition: The set of timed state sequence \(\kappa\) such that \(\kappa(t)=\gamma(t)\) for each \(t\ge0\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\gamma\) a signal over \(2^{\mathrm{AP}}\)
Notation: [$]\llbracket\gamma\rrbracket[/$]

Definition: The set of bipartite timed state sequence \(\kappa\) such that \(\kappa(t)=\gamma(t)\) for each \(t\ge0\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\gamma\) a signal over \(2^{\mathrm{AP}}\)
Notation: [$]\llbracket\gamma\rrbracket^{\mathrm{bp}}[/$]

Definition: The set of signals \(\gamma\) such that \(\gamma\models\phi\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\phi\) a MITL formula
Notation: \(\mathcal S(\phi)\)

Name: A propositional constraint over \(\mathrm{AP}\)
Definition: A set of states over \(\mathrm{AP}\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates

Name: A signal automaton
Definition: \(L\) a finite set of locations
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
Definition2: \(L_0\) the set of inital locations
Conjdef: A tuple
Definition3: \(\alpha\) a function sending locations to propositional constraints
Abbreviation: SA
Definition4: \(X\) a finite set of colcks
Definition5: \(\beta\) a function sending locations to clock constraints
Definition6: \(\Delta\subseteq L\times2^X\times L\) the set of transitions
Definition7: \(\mathcal F\subseteq2^L\) the family of sets of accepting locations

Name: A run of \(A\) on \(\gamma\)
Definition: \(\ell_i\in L\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
\(\gamma\) a signal
Definition2: \((I_i)_{i\in\mathbb N}\) is an interval sequence
Conjdef: A sequence \(\xrightarrow[v_0]{}(\ell_0,I_0)\xrightarrow[v_1]{\lambda_1}(\ell_1,I_1)\dots\) satifsying
Definition3: \(\lambda_i\subseteq X\)
Definition4: initialisation \(\ell_0\in L_0\), \(v_0=\mathbf 0\)
Denoted by: \(\pi\)
Definition5: Consecution: for all \(i\ge 0\), \(\ell_i,\lambda_{i+1},\ell_{i+1})\in\Delta\) and [$]v_{i+1}=(v_i+\abs{I_i})[\lambda_{i+1}\leftarrow 0][/$]
Definition6: Timing: \(v_\pi(t)\models\beta(\ell_\pi(t))\) for all \(t\ge0\)
Definition7: Adequation: \(\gamma(t)\in\alpha(\ell_\pi(t))\) for al \(t\ge0\)

Definition: \(v_i+(t-\text{inf}I_i))\) with \(t\in I_i\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
\(\gamma\) a signal
\(\pi=\xrightarrow[v_0]{}(\ell_0,I_0)\xrightarrow[v_1]{\lambda_1}(\ell_1,I_1)\dots\) a run of \(A\) on \(\gamma\)
Notation: \(v_\pi(t)\)
Conjdef: A sequence

Definition: \(\ell i\) with \(t\in I_i\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
\(\gamma\) a signal
\(\pi=\xrightarrow[v_0]{}(\ell_0,I_0)\xrightarrow[v_1]{\lambda_1}(\ell_1,I_1)\dots\) a run of \(A\) on \(\gamma\)
Notation: \(\lambda_\pi(t)\)
Conjdef: A sequence

Name: An accepting run of \(\mathcal A\) on \(\gamma\)
Definition: a run \(\pi=\xrightarrow[v_0]{}(\ell_0,I_0)\xrightarrow[v_1]{\lambda_1}(\ell_1,I_1)\dots\) of \(A\) on \(\gamma\) such that for all \(F\in\mathcal F\), \(\{i\mid\ell_i\in F\}\) is infinite
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
\(\gamma\) a signal

Name: A signal accepted by \(\mathcal A\)
Definition: A signal admiting an accepted run by \(\mathcal A\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton

Name: The set of signals accepted by \(\mathcal A\)
Page: 4
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A=(L,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
Notation: \(\mathcal {S(A)}\)

Page: 4
Variables: \(\mathrm{AP}\) a set of atomic predicates
\(\mathcal A^i=(L^i,L^i_0,\alpha^i,X^i,\beta^i,\Delta^i,\mathcal F^i)\) a signal automaton
Section: 2
Chapter: Timed-automata-based verification of MITL over Signals
Transitions: \((\ell^1,\ell^2)\to\alpha^1(\ell^1)\land\alpha^2(\ell^2)\)
States: A sequence
Initial: \(L^1_0\times L^2_0\)
Name: The asynchronous product of \(\mathcal A^1\) and \(\mathcal A^2\)
Notation: \(\mathcal {A}^1\times\mathcal A^2\)
Locations: \(L^1\times L^2\)
Labels: the set of \(((\ell^1_i,\ell^2_i),\lambda^1\cup\lambda^2,(\ell^1_j,\ell^2_j))\) \(((\ell^1,\ell^2_i),\lambda^2,(\ell^1,\ell^2_j))\) \(((\ell^1_i,\ell^2),\lambda^1,(\ell^1_j,\ell^2))\) with \((\ell^k_i,\lambda^k,\ell^k_j)\in\Delta^k\), \(\lambda^k\in L^k\)
Clock number: \(X^1\cup X^2\)
Labeling function: \((\ell^1,\ell^2)\to\beta^1(\ell^1)\land\beta^2(\ell^2)\)

Definition: \(L_0\subseteq L^s\)
Page: 6
Section: 2
Variables: \(\mathrm{AP}\) a set of atomic predicates
Definition2: for \((\ell_1,\lambda,\ell_2)\in\Delta\), \(\ell_1\in L^s\) iff \(\ell_2\in L^o\)
Conjdef: \(\mathcal A=(L^s\uplus L^o,L_0,\alpha,X,\beta,\Delta,\mathcal F)\) a signal automaton
Definition3: for each \(\ell\in L_0\), \(x=0\in\beta(\ell)\) for some clock \(x\)
Definition4: for \((\ell_1,\lambda,\ell_2)\in\Delta\), \(\ell_1\in L^s\) there exists \(x\in \lambda\) such that \(x=0\) is a conjunct of \(\beta(\ell_2)\)