Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Efficient controller synthesis for a fragment of MTL_{0,\infty}
Tags: récupéré hasSeenConjDef

Name: A timed word
Definition: A finite or infinite sequence of timed points and actions
Page: 168
Variables: \(\Sigma\) a set of actions

Name: The set of all finite timed words over \(\Sigma\)
Page: 168
Variables: \(\Sigma\) a set of actions
Notation: \(Runs(\Sigma)\)

Name: The set of all infinite timed words over \(\Sigma\)
Page: 168
Variables: \(\Sigma\) a set of actions
Notation: \(InfRuns(\Sigma)\)

Name: A Zeno timed word
Definition: A word which contains infinitely many actions in a finite time
Page: 168
Variables: \(\Sigma\) a set of actions

Name: A Zeno timed word for \(\Sigma'\)
Definition: A word which contains infinitely many actions of \(\Sigma'\) and is time bounded
Page: 168
Variables: \(\Sigma\) a set of actions
\(\Sigma'\)

Name: The set of Zeno timed-words for \(\Sigma'\)
Page: 168
Variables: \(\Sigma\) a set of actions
\(\Sigma'\subseteq\Sigma\)
Notation: \(Zeno(\Sigma')\)

Definition: true
Page: 168
Variables: \(\Sigma\) a set of actions
Notation: \(MTL_{0,\infty}\)
Definition2: \(a\) for \(a\in\Sigma\)
Conjdef: The set containing
Definition3: closed under \(\neg\)
Definition4: closed under \(\land\)
Definition5: closed under \(\bigcirc\)
Definition6: \(\phi_1\mathcal{U}_{\sim d}\phi_2\), for \(\sim\in\{<,\le,\ge,>\}\) and \(d\in\mathbb N\)
Definition7: \(\phi_1\hat{\mathcal{U}}_{\sim d}\phi_2\), for \(\sim\in\{<,\le,\ge,>\}\) and \(d\in\mathbb N\)

Name: Until operators
Page: 169
Context: MTL
Notation: \(\mathcal U\) and \(\hat{\mathcal U}\)

Name: Release operators
Page: 169
Notation: \(\mathcal R\) and \(\hat{\mathcal R}\)

Definition: \(\neg(\neg\phi_1\mathcal U_{\sim d}\neg\phi_2)\)
Page: 169
Variables: \(\phi_1,\phi_2\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)
Notation: \(\phi_1\mathcal R_{\sim d}\phi_2\)

Definition: \(\neg(\neg\phi_1\hat{\mathcal U}_{\sim d}\neg\phi_2)\)
Page: 169
Variables: \(\phi_1,\phi_2\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)
Notation: \(\phi_1\hat{\mathcal R}_{\sim d}\phi_2\)

Definition: \(false\mathcal R_{\sim d}\phi\)
Page: 169
Variables: \(\phi_1\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)
Notation: \(\Box_{\sim d}\phi\)

Definition: \(false\mathcal U_{\sim d}\phi\)
Page: 169
Variables: \(\phi_1\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)
Notation: \(\square_{\sim d}\phi\)

Definition: \(true\hat{\mathcal U}_{\sim d}\phi\)
Page: 169
Variables: \(\phi_1\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)
Notation: \(\hat\lozenge_{\sim d}\phi\)

Name: A bounded operator
Definition: An operator with \(_{\sim d}\), with \(\sim\{\le,<\}\)
Page: 169
Variables: \(\phi\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)

Name: An unbounded operator
Definition: An operator with \(_{\sim d}\), with \(\sim\{\ge,>\}\)
Page: 169
Variables: \(\phi\) operators
\(\sim\in\{<,\le,\ge,>\}\)
\(d\in\mathbb N\)

Definition: the operator is applied to \(\ge0\)
Page: 169
Variables: \(\phi\) operators
Notation: Omitted subscript on MITL operators

Definition: Fragment of \(\mathrm{MTL}_{0,\infty}\) that consists of all formulas in the positive normal form that do not use unbounded until
Page: 169
Notation: \(\mathrm{Safety-MTL}_{0,\infty}\)
Example: \(\square\lozenge_{\le 1}a\)
Example2: \(\square_{\le 1}\lozenge_{\le 1}a\)

Definition: Fragment of MTL\(_{0,\infty}\) that consists of all formulas in the positive normal form that do not use release until
Page: 169
Notation: coSafety-MTL\(_{0,\infty}\)
Example: \(\lozenge\square_{\le 1}a\)
Example2: \(\square_{\le 1}\lozenge_{\le 1}a\)

Question: The negation of the \(coSafety-MTL_{0,\infty}\) formula is
Answer: in Safety-MTL\(_{0,\infty}\)
Page: 169

Definition: always holds
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models true\)

Definition: \(a_i=a\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models a\)

Definition: \(w^i\not\models\phi\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models \neg\phi\)

Definition: \(w^{i+1}\models\phi\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models \circ\phi\)

Definition: \(w^{i}\models\phi\) and \(w^{i}\models\psi\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models\phi\land\psi\)

Definition: there exists \(j\ge i\) \(w^j\models\psi\), \(t_j-t_i\sim d\) and \(w^k\models \phi\) for all \(i\le k\le j\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi,\psi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models \phi\mathcal U_{\sim d}\psi\)

Definition: there exists \(j>i\) \(w^j\models\psi\), \(t_j-t_i\sim d\) and \(w^k\models \phi\) for all \(i<k\le j\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi,\psi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
\(i\in\mathbb N\)
Notation: \(w^i\models \phi\hat{\mathcal U}_{\sim d}\psi\)

Definition: \(w^1\models \phi\)
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
Notation: \(w\models \phi\)

Question: Difference between \(\mathcal U\) and \(\hat{\mathcal U}\)
Answer: \(\hat{\mathcal U}\) does not consider current time
Page: 169
Variables: \(\Sigma\) a set of actions
\(\phi\) a MTL\(_{0,\infty}\) formula
\(w=(t_1,a_1)\dots\) an infinite timed words
Context: MTL

Name: A synthesis problem
Definition: \((\Sigma_c,\Sigma_u)\) with \(\Sigma_c\) disjoint from \(\Sigma_u\)
Page: 169
Chapter: 2
Definition2: \(\phi\) a MTL\(_{0,\infty}\) formula over \(\Sigma_c\cup\Sigma_u\)
Conjdef: A 3-tuple

Name: The game generated by this problem
Definition: Initial state: empty word
Page: 169
Chapter: 2
Variables: \((\phi,\Sigma_c,\Sigma_u)\) a synthesis problem
Definition2: Controller proposes to play some controllable action
Enveronment can let the controller do this, or overtake with a smaller or equal delay and some uncontrollable action

Name: A strategy
Definition: A function mapping \(Runs(\Sigma_c\cup\sigma_u)\)to the pairs \((\tau,a)\) where \(\tau\ge0\) and \(a\in\Sigma_c\)
Page: 169
Chapter: 2
Variables: \((\phi,\Sigma_c,\Sigma_u)\) a synthesis problem

Name: A play consistent with the strategy
Definition: A play \((t_1,a_1)\dots\) such that, for any \(i\), either \(a_{i+1}\in\Sigma_u\) or \(f((t_1,a_1)\dots(t_{i-1},a_{i-1}))=(t_i-t_{i-1},a_i)\)
Page: 169
Chapter: 2
Variables: \((\phi,\Sigma_c,\Sigma_u)\) a synthesis problem
\(f\) a strategy