Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Controller Synthesis for MTL Specifications
Tags: hasSeenConjDef fromImplication
On every note of this deck, unless a note says otherwise:
Chapter: Controller Synthesis for MTL Specifications
Chapter: Controller Synthesis for MTL Specifications

Name: A fair transition system controlling \(\mathcal P\)
Definition: A timed TS \(\mathcal C\) over \((\Sigma,X_{\mathcal P}\cup X_{\mathcal C})\) of granularity \(\mu\) such that all states of \(\mathcal C\) are accepting
Page: 5
Section: 2.2
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
\(\mathcal P\) a plant over \(\tilde\Sigma\),
\(X_{\mathcal C}\) disjoint from \(X_{\mathcal P}\),
\(\mu=(X_{\mathcal P}\cup X_{\mathcal C},m,max)\) a granularity finer than that of the plant.
Name2: Property (C4)

Name: A non-zeno timed word
Definition: An infinite word such that the sequence of time tag is unbounded
Page: 2
Variables: \(\Sigma\) an alphabet

Question: The STS \(\mathcal T=\langle S,s_0,\to\rangle\) is
Answer: \(\langle S,s_0,\to,S\rangle\), each states are assumed to be accepting.
Page: 3
Section: 2

Name: The deterministic version of \(\mathcal T\)
Definition: Set of states \(2^S\)
Page: 3
Variables: \(\mathcal T=\langle S,s_0,\to\rangle\) a STS
Definition2: Initial state \(\{s_0\}\)
Definition3: Transition relation \(S_1\xrightarrow b_D\{s_2\in S\mid \exists s_1\in S_1. s_1\xrightarrow bs_2\}\) with \(S_2\ne\emptyset\).
Abbreviation: \(Det(\mathcal T)\)

Name: A symb-deterministic STS
Definition: A STS \(\mathcal T=\langle S,s_0,\to\rangle\) such that \(s\xrightarrow bs_1\) and \(s\xrightarrow bs_2\) implies \(s_1=s_2\)
Page: 3

Question: Difference between symb-determinism and determinism ?
Answer: symb-determinism authorizes to have two firable transitions, assuming their guards are distinct or that they reset different set of clocks
Page: 4
Variables: \(X\) a set of clock,
\(\Sigma\) an alphabet,
\(\mathcal T=\langle S,s_0,\to\rangle\) a STS

Smaller0: \(\mathcal T\) is deterministic
Greater0: \(\mathcal T\) is symb-deterministic
Page: 4
Chapter: Controller Synthesis for MTL Specifications
Variables: \(X\) a set of clock,
Let \(\Sigma\) an alphabet,
\(\Gamma\) a symbolic alphabetbased on \((\Sigma,X)\)
Let \(\mathcal T=\langle S,s_0,\to\rangle\) a STS over \(\Gamma\)

Name: A MTL formula in positive normal form
Definition: A formula such that negations are only applied to atomic predicates
Page: 4

Name: A Safety-MTL formula
Definition: MTL in positive normal form such that:
-for each instances of the constrained until operator \(\mathcal U_I\), \(I\) has bounded length.
(Note that there are no restriction on the dual-until operator)
Page: 4

Name: A \(\mu\)-controller which controls \(\mathcal P\) against the desired behaviors \(\mathcal L\)
Definition: A \(\mu\)-controller \(\mathcal C\) such that \(\mathcal L^*(\mathcal P||\mathcal C)\subseteq\mathcal L\).
Page: 5
Section: 2.2
Variables: \(\tilde\Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
\(\mathcal P\) a plant over \(\tilde\Sigma\),
\(X_{\mathcal C}\) disjoint from \(X_{\mathcal P}\),
\(\mu=(X_{\mathcal P}\cup X_{\mathcal C},m,max)\) a granularity finer than that of the plant.
\(\mathcal L\subseteq T\Sigma^*\) a specification of desired behaviors
Extra: against is the right word

Name: A \(\mu\)-controller which controls \(\mathcal P\) against the undesired behaviors \(\mathcal L\)
Definition: A \(\mu\)-controller \(\mathcal C\) such that \(\mathcal L^*(\mathcal P||\mathcal C)\) is disjoint from \(\mathcal L\).
Page: 5
Section: 2.2
Variables: \(\tilde\Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
\(\mathcal P\) a plant over \(\tilde\Sigma\),
\(X_{\mathcal C}\) disjoint from \(X_{\mathcal P}\),
\(\mu=(X_{\mathcal P}\cup X_{\mathcal C},m,max)\) a granularity finer than that of the plant.
\(\mathcal L\subseteq T\Sigma^*\) a specification of undesired behaviors

Name: The control problem with fixed resources against desired (resp. undesired) behaviours
Definition: Deciding, given a plant \(\mathcal P\), a specification \(\mathcal L\), and a granularity \(\mu\) finer than that of \(\mathcal P\), whether there exists a \(\mu\)-controller \(\mathcal C\) which controls \(\mathcal P\) against the specification of desired (resp. undesired) behaviours \(\mathcal L\).
Page: 5
Section: 2.2

Name: The control problem with non-fixed resources
Definition: Deciding, given a plant \(\mathcal P\), a specification \(\mathcal L\) whether there exists a granularity \(\mu\) finer than that of \(\mathcal P\) and a \(\mu\)-controller \(\mathcal C\) which controls \(\mathcal P\) against the specification of desired (resp. undesired) behaviours \(\mathcal L\).
Page: 5
Section: 2.2

Definition: whose set of states is \(S\times M^*\) and
Page: 6
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a DCM
Notation: \(G(\mathcal S)\)
Definition2: \((s,x)\xrightarrow {m!}(s',xm)\) for \((s,m!,s')\in\Delta\)
Conjdef: The labelled graph
Definition3: \((s,mx)\xrightarrow {m?}(s',x)\) for \((s,m?,s')\in\Delta\)

Name: \(s_{halt}\) is reachable in \(\mathcal S\)
Definition: There exists a path from \((s_0,\epsilon)\) to \((s_{halt},x)\) in \(G(\mathcal S)\)
Page: 6
Section: 3
Variables: \((S,s_0,s_{halt},M,\Delta)\) a DCM

Question: The reachability problem for DCM is
Answer: undecidable
Page: 6
Section: 3
Index: 1
Kind: Prop

Question: The control problem with non-fixed resources for MTL specification over finite words representing desired behaviours is
Answer: undecidable
Page: 6
Section: 3
Index: 1
Kind: Theo

Question: The control problem with non-fixed resources for MTL specification over finite words representing undesired behaviours is
Answer: undecidable
Page: 6
Section: 3
Index: 1
Kind: Theo

Name: A DCM in normal form (w.r.t. to reachability)
Definition: \(s_{halt}\) is the single state with no outgoing transition,
Page: 6
Section: 3
Definition2: there is no cycle in \((S,\delta)\) in which every edge is labelled by a write action
Conjdef: A DCM \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) such that
Definition3: If the unique maximal path in \(G(\mathcal S)\) is infinite, the size of the channel content is unbounded.

Name: The encoding of the maximal correct path as a timed word
Definition: there exists \((s_i)\) such that \(s_1=s_0\) and \((s_1,a_i,s_{i+1})\in\Delta\)
Page: 6
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a DCM in normal form
Definition2: Each \(t_i\) are disjoint
Conjdef: A word \((a_i,t_i)_{i\in \mathbb N}\) over \(\{m?,m!\mid m\in M\}\) such that
Definition3: the \(m!\) and \(m?\) comes in pair, separated by an interval of 1 (apart at the last time unit, where sent message may not be read)

Name: Non-strict version of \(\lozenge\)
Definition: \(\phi\lor\lozenge_I\phi\)
Page: 7
Section: 3
Variables: \(\phi\) a formula,
\(I\) an interval
Notation: \(\overline\lozenge\phi \)
Extra: Not assumed that \(0\in I\)

Name: Non-strict version of \(\square\)
Definition: \(\neg\overline\lozenge_I\neg\phi\)
Page: 7
Section: 3
Variables: \(\phi\) a formula,
\(I\) an interval
Notation: \(\overline\square\phi \)

Name: A validity function over \(\Sigma\)
Definition: A function \(f:2^\Sigma\to \left(2^{\left(2^\Sigma\right)} \setminus \emptyset\right)\) such that \(f(U)\subseteq 2^U\)
Page: 8
Section: 4
Variables: \(\Sigma\) an alphabet
Denoted by: \(val\)

Name: A strategy in \(\mathcal T\) respecting \(val\)
Definition: \(\epsilon\in D\),
Page: 8
Section: 4
Variables: \(\Sigma\) an alphabet,
\(\mathcal T=\langle S,s_0,\to\rangle\) a symb-deterministic STS over a symbolic alphabet \(\Gamma\),
\(val\) a validity function over \(\Gamma\)
Definition2: for all \(\gamma\in D\), \(f(\gamma)\in val(enabled_{\mathcal T}(state_{\mathcal T}(\gamma)))\)
Conjdef: A pair \(D\subseteq \mathcal L^*_{symb}(\mathcal T)\) and \(f:D\to 2^\Gamma\) such that
Definition3: for all \(\gamma\in D\), and \(b\in f(\gamma)\)and \(\gamma\cdot b\in D\).

Definition: The last state of the only run whose trace is \(\gamma\)
Page: 3
Section: 2
Variables: \(\mathcal T\) a symb-determinstic STS,
\(\gamma\) a finite trace
Notation: \(state_{\mathcal T}(\gamma)\)

Name: The set of plays of \(f\)
Definition: The set of words in \(\mathcal L_{symb}(\mathcal T)\) that are consistent with the strategy \(f\)
Page: 8
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
\((\mathcal H,L)\) a timed game over \(\Gamma\)
\(f\) a strategy
Notation: \(plays(f)\)

Name: A finite-state strategy
Definition: A strategy whose set of plays is of the form \(\mathcal L_{symb}(\mathcal T_{fin})\) for a symb-deterministic finite-state STs \(\mathcal T_{fin}\).
Page: 8
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
\((\mathcal H,L)\) a timed game over \(\Gamma\)

Name: A timed game over finite (resp. infinite) words
Definition: \(\mathcal L\subseteq T\Sigma^\infty\) is a timed language over finite (resp infinite) words.
Page: 8
Section: 4
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clock,
\(\gamma\) a granularity
Definition2: \(\mathcal A\) is an atomic consistent symb-determinstic TA over a symbolic alphabet \(\Gamma\) based on \((\Sigma,X)\)
Conjdef: A pair
Denoted by: \(\mathbb G\)

Name: An atomic TA
Definition: A TA such that each clock constraint is atomic w.r.t. the granularity.
Page: 8
Section: 4
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clock,
\(\gamma\) a granularity

Name: A consistent TA
Definition: \(tw(\mathcal L^\omega_{symb}(\mathcal A))\subseteq T\Sigma^\omega\)
Page: 8
Section: 4
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clock,
Definition2: for every \(\gamma\in\mathcal L_{symb}(\mathcal T(\mathcal A))\), \(tw(\gamma)\ne\emptyset\)
Conjdef: A TA \(\mathcal A\) such that both

Definition: The STS corresponding to \(\mathcal A\) where all states are considered accepting.
Page: 3
Section: 2
Variables: \(\mathcal A\) a TA
Notation: \(\mathcal {T(A)}\)