Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / MightyL: A compositional Translation from MITL to Timed Automata
Tags: récupéré MissingMedia toAutomata

Name: MITL over signals
Page: 422
Section: 1
Name2: MITL with continuous semantic

Name: Dual next operator of \(\phi\)
Definition: \(\neg\mathbf X_I\neg\phi\)
Page: 424
Section: 1
Variables: \(\phi\) a MTL variable,
\(I\) a closed interval of natural bounds
Notation: \(\bar{\mathbf X}_I\phi\)

Definition: Fragments of \(MITL\) restricted to intervals one of endpoints is \([0\) or \(+\infty)\)
Page: 424
Section: 1
Notation: \(MITL_{0,\infty}\)

Name: Generalised Büchi timed automaton
Definition: \(L\) a finite set of locations
Page: 424
Section: 2
Definition2: \(\Sigma\) a finite alphabet
Conjdef: The tuple
Definition3: \(\ell_0\in L\) the initial location
Abbreviation: GBTA
Definition4: \(\Delta\subseteq L\times\Sigma\times\mathcal G(X)\times 2^X\times L\) the transition relation
Definition5: \(\mathcal F=\{F_1,\dots F_n\}\) with \(F_i\subseteq L\) the set of sets of final locations

Name: The synchronisation of the \(\mathcal A^i\)
Definition: \(\prod L^i\)
Page: 425
Section: 2
Variables: \(\mathcal A^i=(L^i,\Sigma,\ell^i_0,\Delta^i,\mathcal F^i)\) GBTAs
Notation: \(\prod\mathcal A^i\)
Definition2: \((\ell_0^i)_{i}\)
Conjdef: The GBTA
Definition3: \(((\ell_1^i)_i,\sigma,\bigwedge g^i,\bigcup R^i,(\ell_2^i)_i)\) if \((\ell_1^i,\sigma,g^i,R^i,\ell^i_2)\in\Delta^i\)
Definition4: the set of \(\prod S^i\), with one \(S^i\in\mathcal F^i\), every other \(S^i=L^i\)

Definition: containing \(\top\), \(\bot\)
Page: 425
Section: 2
Variables: \(L\) a set of locations
Context: MITL et TA
Notation: \(\Gamma(L)\)
Definition2: closed under \(\lor\) and \(\land\)
Conjdef: The set
Definition3: containing elements of \(L\)
Definition4: closed under \(\le,<,>,\ge\)
Definition5: closed under \(x.\gamma\), for gamma in this set

Name: An One-clock alternating automaton
Definition: \(L\) a finite set of locations
Page: 425
Section: 2
Definition2: \(\Sigma\) a finite alphabet
Conjdef: The tuple
Definition3: \(\ell_0\in L\) initial location
Abbreviation: OCATA
Definition4: \(\delta:L\times \Sigma\to\Gamma(L)\) transition function
Definition5: \(F\subseteq L\) set of final locations

Name: A state
Definition: An element of \(L\times\mathbb R^{\ge0}\)
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA

Definition: if \(\gamma=\top\)
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation
\(M\) a set of states
Notation: \(M\models_v\gamma\)
Definition2: if \(\gamma =\ell\): \((\ell,v)\in M\)
Conjdef: Either
Definition3: if \(x\bowtie c\): \(x\bowtie c\)
Definition4: If \(x.\gamma\):\(M\models_0\gamma\)
Definition5: If \(\gamma=\gamma_1\land\gamma_2\): \(M\models_v\gamma_1\) and \(M\models_v\gamma_2\)
Definition6: If \(\gamma=\gamma_1\lor\gamma_2\): \(M\models_v\gamma_1\) or \(M\models_v\gamma_2\)

Name: A model of \(\gamma\) for \(v\)
Definition: A set of states \(M\) such that \(M\models_v\gamma\)
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation

Name: A minimal model of \(\gamma\) for \(v\)
Definition: A model of \(\gamma\) for \(v\) minimal for inclusion
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation

Name: A run of \(\mathcal A\) over \(\rho\)
Definition: vertices of the form \((\ell,v,i)\in L\times\mathbb R^+\times\mathbb N\)
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation
\(\rho=(\sigma_i,\tau_i)_i\) a timed-word
Definition2: \((\ell_0,0,0)\) as root
Conjdef: A DAG
Definition3: for every vertex \((\ell,v,i)\), a minimal model \(M\) of the formula \(\delta(\ell,\sigma_{i+1})\) with respect to \(v+(\tau_{i+1}-\tau_i)\) and we have an edge \((\ell,v,i)\to(\ell',v',i+1)\) for every state \((\ell',v')\in M\)

Name: An accepting run of \(\mathcal A\) over \(\rho\)
Definition: A run such that each infinite path contains infinitely many accepting state
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation
\(\rho=(\sigma_i,\tau_i)_i\) a timed-word

Name: A configuration
Definition: A finite set of states
Page: 425
Section: 2
Variables: \(\mathcal A\) an OCATA
\(\gamma\in\Gamma(L)\)
\(v\) a clock valuation

Name: Set of locations of \(A_\phi\)
Definition: \(\phi_{init}\) (initial)
Page: 426
Section: 2
Variables: \(\phi\in MITL\)
Definition2: subformulae of \(\phi\) in NNF, whose outermost operator is \(\mathrm{U_I}\)
Conjdef: All of
Definition3: \(\psi^r\) for each subformulae \(\psi\) of \(\phi\) whose outermost operator is \(\mathrm{X_I}\) or  \(\bar{\mathrm{X_I}}\)
Definition4: subformulae of \(\phi\) in NNF, whose outermost operator is \(\mathrm{R_I}\) (final)

Question: \(\delta(\phi_{init},\sigma)\) equals
Answer: \(x.\delta(\phi,\sigma)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)
Context: \(A_\phi\)

Question: \(\delta(\top,\sigma)\) equals
Answer: \(\top\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\bot,\sigma)\) equals
Answer: \(\bot\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(p,\sigma)\) equals
Answer: \(\top\) if \(p\in\sigma\), \(\bot\) otherwise
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\neg p,\sigma)\) equals
Answer: \(\top\) if \(p\not\in\sigma\), \(\bot\) otherwise
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\phi_1\lor\phi_2,\sigma)\) equals
Answer: \(\delta(\phi_1,\sigma)\lor\delta(\phi_2,\sigma)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\phi_1\land\phi_2,\sigma)\) equals
Answer: \(\delta(\phi_1,\sigma)\land\delta(\phi_2,\sigma)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\phi_1\mathrm U_I\phi_2,\sigma)\) equals
Answer: \((x.\delta(\phi_2,\sigma)\land x\in I)\lor(x.\delta(\phi_1,\sigma)\land \phi_1\mathrm{U_I}\phi_2\land x\le \text{sup }I)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\phi_1\mathrm R_I\phi_2,\sigma)\) equals
Answer: \((x.\delta(\phi_2,\sigma)\lor x\not\in I)\land(x.\delta(\phi_1,\sigma)\lor\phi_1\mathrm{R_I}\phi_2\lor x>\text{sup }I)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\mathrm X_I\phi,\sigma)\) equals
Answer: \(x.(\mathrm X_I\phi)^r\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta(\mathrm {\bar X}_I\phi,\sigma)\) equals
Answer: \(x.(\mathrm {\bar X}_I\phi)^r\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta((\mathrm {\bar X}_I\phi)^r,\sigma)\) equals
Answer: \(x\not\in I\lor x.\delta(\phi,\sigma)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Question: \(\delta((\mathrm { X}_I\phi)^r,\sigma)\) equals
Answer: \(x\in I\land x.\delta(\phi,\sigma)\)
Page: 427
Section: 2
Variables: \(\phi\in MITL\)
\(\sigma\in\Sigma\)

Name: A very-weak OCATA
Definition: An OCATA with a partial order on its locations such that all locations appearing in \(\delta(\ell,\sigma)\) are bounded above by \(\ell\) in this order.
Page: 427
Section: 2

Name: A parent of \(\ell\)
Definition: A state \(\ell'\) such that \(\delta(\ell',\sigma)\ni \ell\) for some \(\sigma\in\Sigma\)
Page: 427
Section: 2
Variables: \(\phi\) a MITL formula
\(\ell\) locations of \(A_\phi\)
\(\sigma\in\Sigma\)
Typ: At most one

Definition: \(\ell\) is a subformula of \(\ell'\)
Page: 427
Section: 2
Variables: \(\phi\) a MITL formula
\(\ell,\ell'\) locations of \(A_\phi\)
Notation: \(\ell<\ell'\)

Name: A temporal subformula
Definition: A subformula of \(\phi\) whose outermost operator is temporal
Page: 427
Section: 2
Variables: \(\phi\) a MITL formula

Name: The set of temporal subformulae of \(\phi\)
Page: 427
Section: 2
Variables: \(AP\) a set of predicate
\(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
Notation: \(\Phi\)

Definition: the set of atomic propositions \(p_\xi\in AP_{\phi}\) such that \(\xi\) is a top-level temporal subformula of \(\psi\), not occurring below any \(\mathrm U_I\) nor \(\mathrm R_I\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
\(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
Notation: \(\mathcal P_\phi\)

Definition: The set of \(p_{\psi}\) for each \(\psi\in\Phi\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
Notation: \(AP_\phi\)

Name: A Hintikka sequence of \(\phi\)
Definition: A timed-word over \(2^{AP\cup AP_\phi}\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)

Definition: The sequence, similar to \(\rho\), without the letters from \(AP_{\phi}\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\rho\) a Hintikka sequence of \(\phi\)
Notation: \(\mathrm{proj_{AP}}(\rho)\)

Definition: The formula obtained from \(\psi\) by replacing each \(\xi\in\mathcal P_\psi\) by \(p_{\xi}\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\psi\) a subformula of \(\phi\)
Notation: \(\bar\psi\)

Definition: \(\bigwedge_{\xi\in\mathcal P(\phi)}\neg p_{\xi}\)
Page: 428
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\psi\) a subformula of \(\phi\)
Notation: \(*\psi\)
Applied to3: Do not pull the trigger of \(\psi\)

Definition: \(\neg\bar\psi\land*\psi\)
Page: 429
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\psi\) a subformula of \(\phi\)
Notation: \(\sim\psi\)

Definition: \(\mathrm{mm}(\bar\psi)\)
Page: 429
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\psi\) a subformula of \(\phi\)
Notation: \(\hat\psi\)

Page: 429
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\psi\) a subformula of \(\phi\)
Notation: \(\mathrm{mm}(\psi)\)
Conjdef: Defined recursively on \(\psi\)
Applied to3: A formula, equisatisfiable with \(\psi\), ensuring only minimal models

Definition: A Büchi automaton with two states \(0\) and \(1\).
State 1 means \(\psi_2\) must be seen in the futur, while remaining in \(\psi_1\)
Page: 429
Section: 2
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\xi=\psi_1\mathrm U\psi_2\) a subformula of \(\phi\)
\(p\in AP\)
Notation: \(\mathcal C_\xi\)

Question: \(\mathcal C_\xi\)
Page: 429
Section: 4
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\xi=\phi_1\mathrm U_{[0,a]}\phi_2\) a subformula of \(\phi\)
\(p\in AP\)

Question: \(\mathcal C_\xi\)
Page: 429
Section: 4
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\xi=\phi_1\mathrm R_{[0,a]}\phi_2\) a subformula of \(\phi\)
\(p\in AP\)

Question: \(\mathcal C_\xi\)
Page: 429
Section: 4
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\xi=\phi_1\mathrm R_{[0,+\infty)}\phi_2\) a subformula of \(\phi\)
\(p\in AP\)

Page: 429
Section: 4
Variables: \(AP\) a set of predicate
Let \(\phi\) a MITL formula in NNF
\(A_\phi\) the OCATA obtained from \(\phi\)
\(\ell\) a location of \(A_\phi\)
\(v\ge0\)
\(\gamma\in\Gamma(L)\)
\(M\) a minimal model of \(\gamma\) with respect to \(v\)
Notation: \(\mathrm{trig}_\psi(M,\gamma,v)\)
Applied to3: The set of triggers activated

Name: A state in interval semantic
Definition: A pair \((\ell,[\alpha,\beta])\) with \(\alpha\le\beta\)
Page: 434
Section: 4
Variables: \(A\) an OCATA
Applied to3: The model admets elements in state \(\ell\) at times \(\alpha\), \(\beta\) and potentially in \((\alpha,\beta)\)

Name: The merges of the \((\ell,[\alpha_i,\beta_i])\)
Definition: The state \((\ell,[\min \alpha_i,\max\beta_i])\)
Page: 434
Section: 4
Variables: \(A\) an OCATA,
\((\ell,[\alpha_i,\beta_i])\) states in interval semantic

Definition: The set of subsets of \(\Sigma\) containing \(\sigma\)
Page: 426
Section: 2
Variables: \(\Sigma\) an alphabet
\(\sigma\in\Sigma\)
Notation: \(\Sigma_\sigma\)

Name: Pulling the trigger \(p_\psi\)
Definition: Setting \(p_\psi\) to True
Page: 428
Section: 2
Variables: \(\phi\) in MITL
\(\psi\) a subformula
Applied to3: \(\psi\) is required to hold at this point.

Question: When the trigger \(p_\psi\) is not pulled
Answer: no requirements exists
Page: 428
Section: 2
Variables: \(\phi\) in MITL
\(\psi\) a subformula

Name: Having an obligation for \(\xi\)
Definition: \(\mathcal C_X\) is in location 1
Page: 429
Section: 2
Variables: \(\phi\) in MITL
\(\xi\in\Phi\) a subformula
Definition2: \(\mathcal C_{init}\) or some \(\mathcal C_\psi\) with \(p_\xi\in\mathcal P_\phi\) has triggerred \(p_\xi\), and it has not been satisfied

Page: 429
Section: 2
Variables: \(\phi\) in MITL
\(\xi\in\Phi\) a subformula
Notation: \(\mathcal C_{init}\)

Page: 429
Section: 2
Variables: \(\phi\) in MITL
\(\xi=\phi_1\mathcal U\phi_2\in\Phi\) a subformula
Notation: \(\mathcal C_{\xi}\)

Page: 429
Section: 2
Variables: \(\phi\) in MITL
\(\xi=\phi_1\mathcal R\phi_2\in\Phi\) a subformula
Notation: \(\mathcal C_{\xi}\)