Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Timed Control Synthesis for External Specifications
Tags: hasSeenConjDef fromImplication compare defToAut fromMath mathToSee récupéré toBinaryRelation

Name: An open reactive system
Definition: A system that interacts with its environment.
Page: 1

Name: A transition system over \(A\)
Definition: \(Q\) a set of states,
Page: 3
Section: 2
Variables: \(A\) an alphabet
Definition2: \(q_0\in Q\) the initial state
Conjdef: A tuple with
Definition3: \(\to\subseteq Q\times A\times Q\) its transition relation
Denoted by: \(\mathcal T\)

Name: A run of \(\mathcal T\) on \(\alpha\)
Definition: A function \(f:pre(\alpha)\to Q\) such that \(f(\epsilon)=q_0\) and \(f(w)\xrightarrow af(wa)\) for each \(wa\in pre(\alpha)\)
Page: 3
Section: 2
Variables: \(A\) an alphabet,
\(\alpha\in A^\infty\)
\((Q,q_0,\to)\) a TS over \(A\)
Denoted by: \(\rho\)

Definition: The set of words in \(A^\omega\) on which \(\mathcal T\) has a run.
Page: 3
Section: 2
Variables: \(A\) an alphabet,
\((Q,q_0,\to)\) a TS over \(A\)
Notation: \(L_{sym}(\mathcal T)\)

Definition: The set of words in \(A^*\) on which \(\mathcal T\) has a run.
Page: 3
Section: 2
Variables: \(A\) an alphabet,
\((Q,q_0,\to)\) a TS over \(A\)
Notation: \(L_{sym}^*(\mathcal T)\)
Extra: No notion of acceptance here

Definition: \(L_{sym}^*(\mathcal T)\cup L_{sym}(\mathcal T)\)
Page: 3
Section: 2
Variables: \(A\) an alphabet,
\((Q,q_0,\to)\) a TS over \(A\)
Notation: \(L_{sym}^\infty(\mathcal T)\)

Name: A deterministic TS
Definition: A TS such that \(q\xrightarrow aq'\) and \(q\xrightarrow aq''\) implies \(q '=q''\)
Page: 3
Section: 2

Name: An \(\omega\)-automaton over \(A\)
Definition: A pair \((\mathcal{T,F})\) where \(\mathcal T\) is a finite state transition system over \(A\), and \(\mathcal F\) is an acceptance condition.
Page: 3
Section: 2
Variables: \(A\) an alphabet
Denoted by: \(\mathcal A\)

Name: A Büchi condition
Definition: A subset of \(Q\)
Page: 3
Section: 2
Variables: \(\mathcal T=(Q,q_0,\to)\) a transition system

Name: A parity condition
Definition: A function \(f:Q\to \{0,\dots,d\}\), where \(d\in\mathbb N\).
Page: 3
Section: 2
Variables: \(\mathcal T=(Q,q_0,\to)\) a transition system
Name2: A Mostowski condition
Denoted by: \(ind\)

Name: The index of \(q\)
Definition: \(ind(q)\)
Page: 3
Section: 2
Variables: \(\mathcal T=(Q,q_0,\to)\) a transition system,
\(ind:Q\to \{0,\dots,d\}\) a parity condition,
\(q\in Q\)

Name: An accepting run
Definition: A run \(\rho\) such that \(\min\{ind(q)\mid q\in inf(\rho)\}\) is even
Page: 3
Section: 2
Variables: \(\mathcal T=(Q,q_0,\to)\) a transition system,
\(ind:Q\to \{0,\dots,d\}\) a parity condition,

Name: An accepting run
Definition: A run \(\rho\) such that \(inf(\rho)\) intersects \(F\)
Page: 3
Section: 2
Variables: \(\mathcal T=(Q,q_0,\to)\) a transition system
\(F\subseteq Q\) a Büchi condition

Name: An accepting word
Definition: A word which is the label of an infinite run
Page: 3
Section: 2
Variables: \((\mathcal T,\mathcal F)\) an \(\omega\)-automaton,

Name: The set of words accepted by \(\mathcal A\)
Page: 3
Section: 2
Variables: \(\mathcal A=(\mathcal T,\mathcal F)\) an \(\omega\)-automaton,
Notation: \(L_{sym}(\mathcal A)\)

Name: A \(\omega\)-regular language
Definition: \(L_{sym}(\mathcal A)\) for some \(\omega\)-automaton \(\mathcal A\)
Page: 3
Section: 2

Name: A constraint over \(X\)
Definition: A Boolean combination of \(x\sim c\) for \(c\in\mathbb Q_{\ge0}\), \(x\in X\) \(\sim\) being \(\le\) or \(\ge\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks
Name2: A guard over \(X\)

Name: A valuation over \(X\)
Definition: A map \(X\to\mathbb R_{\ge 0}\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks
Denoted by: \(v\)

Name: The set of valuations over \(X\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks
Notation: \(val(X)\)

Name: \(v\) satisfies \(g\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks,
\(v\) a valuation
\(g\) a constraint
Notation: \(v\models g\)

Name: A complete set of constraints
Definition: A set \(S\) of constraint such that [$]\bigcup_{g\in S}\llbracket{}g
\rrbracket=val(X)[/$]
Page: 3
Section: 2
Variables: \(X\) a set of clocks,

Definition: \(x\mapsto v(x)+t\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks,
\(v\) a valuation,
\(t\in\mathbb R_{\ge 0}\)
Notation: \(v+t\)

Name: The 0 valuation
Definition: \(x\mapsto 0\)
Page: 3
Section: 2
Variables: \(X\) a set of clocks
Notation: \(\mathbf 0\)

Definition: \(x\mapsto 0\) if \(x\in Y\) and \(x\mapsto v(x)\) otherwise
Page: 3
Section: 2
Variables: \(X\) a set of clocks,
\(Y\subseteq X\),
\(v\) a valuation over \(X\)
Notation: \(v[0/Y]\)

Name: A granularity
Definition: \(X\) a finite set of clock,
Page: 4
Section: 2
Definition2: \(m\in\mathbb N\)
Conjdef: A tuple \((X,m,max)\) with
Definition3: \(max:X\to\mathbb Q_{\ge0}\)
Denoted by: \(\mu\)

Name: A \(\mu\)-granular constraint
Definition: A constraint whose clocks belong to \(X\), each constant used is an integral multiple of \(\frac1m\) and each clock \(x\) is never compared to a constant larger than \(max(x)\).
Page: 4
Section: 2
Variables: \(\mu=(X,m,max)\) a granularity

Name: The set of \(\mu\)-granular constant
Page: 4
Section: 2
Variables: \(\mu=(X,m,max)\) a granularity
Notation: \(\mathcal G(\mu)\)

Page: 4
Definition: \(X\supseteq X'\), \(m'|m\) and \(max(x)\ge max'(x)\) for each \(x\in X'\)
Section: 2
Variables: \(\mu=(X,m,max)\)
\(\mu'=(X',m',max')\) granularities
Notation: \(\mu'\le\mu\)
Name: \(\mu\) is finer than \(\mu'\)
Extra: Checked. The finer is «greatr than»

Name: The granularity of \(S\)
Definition: The least granularity \(\mu\) such that each constraint of \(S\) is \(\mu\)-granular
Page: 4
Section: 2
Variables: \(S\) a finite set of constraint

Definition: \((\bigcup X_i,lcm(m_i\mid i),x\mapsto max(max_i(x)\mid i))\) with \(max_i(x)=0\) for \(i\not\in X_i\)
Page: 4
Section: 2
Variables: \(\mu_i=(X_i,m_i,max_i)\) granularities
Notation: \(\mu_1+\mu_2\)

Name: A timed word over \(\Sigma\)
Definition: An element of \((\Sigma\times\mathbb R_{>0})^{\infty}\) which is monotone and progressive.
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet
Denoted by: \(\sigma\)

Name: A monotonic element \(\sigma\in (\Sigma\times\mathbb R_{>0})^{\infty}\)
Definition: An element \(\sigma\in (\Sigma\times\mathbb R_{>0})\) such that, for each successive pair of letters \((a,t)\cdot (b,t')\) occuring in \(\sigma\), \(t<t'\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet

Name: A progressive element \(\sigma\) of \((\Sigma\times\mathbb R_{>0})^{\infty}\)
Definition: An element such that, for each \(t>0\), there exists a letter \((a,t')\) in \(\sigma\) such that \(t'>t\).
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet

Name: The set of infinite timed words over the alphabet \(\Sigma\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet
Notation: \(T\Sigma^\omega\)

Name: The set of finite timed words over the alphabet \(\Sigma\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet
Notation: \(T\Sigma^*\)

Definition: The time stamp of the last action in \(\tau\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet,
\(\tau\in T\sigma^*\)
Notation: \(time(\tau)\)

Name: A symbolic alphabet based on \((\Sigma,X)\)
Definition: A finite subset of \(\Sigma\times \mathcal G(X)\times 2^X\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks
Denoted by: \(\Gamma\)

Name: The granularity of \(\Gamma\)
Definition: The granularity of the set of constraints used in \(\Gamma\).
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
\(\Gamma=\Sigma\times \mathcal G(X)\times 2^X\) a symbolic alphabet based on \((\Sigma,X)\)

Name: A symbolic word
Definition: An element of \(\Gamma^\infty\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
\(\Gamma=\Sigma\times \mathcal G(X)\times 2^X\) a symbolic alphabet based on \((\Sigma,X)\)
Denoted by: \(\gamma\)

Definition: The set of words \(\sigma\) such that:
-\(|\sigma|=|\gamma|\),
-there exists a sequence of valuations, given by \(\eta: pre(\sigma) \to val (X)\), such
that \(\eta(\epsilon)=0\), and for each prefix \(\tau\cdot (a, t)\) of \(\sigma\) and \(\delta\cdot (b, g, Y )\) of \(\gamma\), with \(|\tau|=|\delta|\) we have:
--\(a=b\),
--\(\eta(\tau)+(t-time(\tau))\models g\) and
--\(\eta(\tau\cdot (a,t))=(\eta(\tau)+(t-time(\tau)))[0/Y]\)
Page: 4
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
\(\Gamma=\Sigma\times \mathcal G(X)\times 2^X\) a symbolic alphabet based on \((\Sigma,X)\),
\(\gamma\) a symbolic word
Notation: \(tw(\gamma)\)

Name: A timed transition system over \((\Sigma,X)\)
Definition: A transition system over a symbolic alphabet based on \((\Sigma,X)\)
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
Denoted by: \(\mathcal T\)

Definition: \(tw(L_{sym}(\mathcal T))\)
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
\(\mathcal T\) a timed transition system over \((\Sigma,X)\)
Notation: \(L(\mathcal T)\)

Definition: \(tw(L^*_{sym}(\mathcal T))\)
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,
\(\mathcal T\) a timed transition system over \((\Sigma,X)\)
Notation: \(L^*(\mathcal T)\)

Name: A timed-\(\omega\)-automaton
Definition: An \(\omega\)-automaton over a symbolic alphabet based on \((\Sigma,X)\)
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks,

Name: A timed \(\omega\)-regular language
Definition: A timed language recognized by a timed \(\omega\)-automaton
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,

Name: A deterministic timed transition system
Definition: A TS \((Q,q_0,\to)\) such that we never have two distinct transitions \(q\xrightarrow[Y]{a,g_1}q_1\) and \(q\xrightarrow[Y']{a,g_2}q_2\) with [$]\llbracket{}g_i
\rrbracket[/$] intersecting.
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
Name2: A time deterministic timed transition system

Page: 5
Variables: \(\Sigma\) an alphabet,
Let \(X_i\) sets of clocks,
Let \(\mathcal T_i=(Q_i,q_0^i,\to_i)\) be TS over \((\Sigma,X_i)\)
Section: 2
Transitions: \((p_1,p_2)\xrightarrow[Y]{a,g}(q_1,q_2)\) iff \(p_i\xrightarrow[Y_1]{a,g_i}_iq_i\), with \(g=\bigwedge g_i\) and \(Y=\bigcup Y_i\).
Name: The synchronized product of \(\mathcal T_1\) and \(\mathcal T_2\)
Notation: \(\mathcal T_1||\mathcal T_2\)
Locations: \((\Pi Q_i, (q_0^1,q_0^2), \to)\) with
Typ: A TS over \((\Sigma,\bigcup X_i)\)

Smaller0: the \(X_i\)'s are disjoint
Greater0: \(L(\mathcal T_1||\mathcal T_2)=L(\mathcal T_1)\cap L(\mathcal T_2)\)
Page: 5
Section: 2
Variables: \(\Sigma\) an alphabet,
\(X_i\) sets of clocks,
\(\mathcal T_i=(Q_i,q_0^i,\to_i)\) be TS over \((\Sigma,X_i)\)

Name: A partitionned alphabet
Definition: A pair of distinct sets \((\Sigma_C,\Sigma_E)\)
Page: 5
Section: 3
Denoted by: \(\tilde\Sigma\)

Name: Its controllable actions
Definition: \(\Sigma_C\)
Page: 5
Section: 3
Variables: \((\Sigma_C,\Sigma_E)\) a partitionned alphabet

Name: Its environment actions
Definition: \(\Sigma_E\)
Page: 5
Section: 3
Variables: \((\Sigma_C,\Sigma_E)\) a partitionned alphabet

Name: A plant over \(\tilde\Sigma\)
Definition: A deterministic, finite-state timed transition system over \(\Sigma\)
Page: 5
Section: 3
Variables: \(\tilde\Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
Denoted by: \(\mathcal P\)

Definition: \(\Sigma_C\cup\Sigma_E\)
Page: 5
Section: 3
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
Notation: \(\Sigma\)

Definition: The set of clocks used in \(\mathcal P\)
Page: 5
Section: 3
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
\(\mathcal P\) a plant over \(\tilde\Sigma\)
Notation: \(X_{\mathcal P}\)

Name: A \(\mu\)-controller for \(\mathcal P\)
Definition: A timed TS \(\mathcal C\) over \((\Sigma,X_{\mathcal P}\cup X_{\mathcal C})\) of granularity \(\mu\) satisfying:
-(C1),
-(C2, non-restricting),
-(C3, non-blocking) and
-(C4, fairness)
Page: 5
Section: 3
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

Name: A transition system controlling \(\mathcal P\) satisfying (C1)
Definition: A timed TS \(\mathcal C\) over \((\Sigma,X_{\mathcal P}\cup X_{\mathcal C})\) of granularity \(\mu\) such that \(\mathcal C\) has resets only in \(X_{\mathcal C}\)
Page: 5
Section: 3
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.

Name: A non-restricting 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:
-Whenever \(\tau\in L(\mathcal P||\mathcal C)\) and \(\tau\cdot(e,t)\in L(\mathcal P)\) with \(e\in\Sigma_E\), then \(\tau\cdot (e,t)\in L(\mathcal P||\mathcal C)\)
Page: 5, 5,
Section: 3, 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.
I.e. the environment can do everything that it could before
Name2: Property (C2)

Name: Control synthesis for specified granularity against undesired behaviours
Definition: Does there exists a \(\mu\)-controller \(\mathcal C\) for \(\mathcal P\) such that \(L(\mathcal P||\mathcal C)\) is disjoint from \(L(\mathcal A_s)\)
Page: 5
Section: 3
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
\(\mathcal P\) a plant over \(\tilde\Sigma\),
\(\mu=(X_{\mathcal P}\cup X_{\mathcal C},m,max)\) a granularity finer than that of the plant.
\(\mathcal A_s\) a timed automaton over \(\sigma\) as a specification of undesired behaviours
Index: 1
Kind: Def

Question: Control synthesis for specified granularity against undesired behaviours is
Answer: decidable and a finite controller can be synthetized
Page: 6
Section: 3
Index: 1
Kind: Theo

Name: The equivalence relation generated by \(\mu\)
Definition: \(v(x),v'(x)>max(x)\), or
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity
Definition2: \(\lfloor v(x)\rfloor=\lfloor v'(x)\rfloor\) and \(\{v(x)\}=0\) iff \(\{v'(x)\}=0\).
Conjdef: The relation between valuations \(v,v'\) such that, for each \(x\in X\), either

Name: An atomic set of valuations for \(X\) w.r.t. \(\mu\)
Definition: An equivalence class of the set of valuations under the equivalence relation generated by \(\mu\).
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity

Name: A region of \(\mu\)
Definition: \(v(x),v'(x)\le max(x)\) iff \(v(y),v'(y)\le max(y)\),
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity
Definition2: \(\{v(x)\}=\{v(y)\}\) iff \(\{v'(x)\}=\{v'(y)\}\),
Conjdef: An equivalence class of valuations \(v,v'\) where, for each pair of clocks \(x,y\in X\):
Definition3: \(\{v(x)\}<\{v(y)\}\) iff \(\{v'(x)\}<\{v'(y)\}\).
Definition4: \(v,v'\) belongs in the same atomic set of valuations.

Smaller0: \(v,v'\) belongs to the same atomic set of valuations
Greater0: \(v\) and \(v'\) satisfy exactly the same guards in \(\mathcal G(\mu)\)
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity,
\(v,v'\) valuations

Name: \(atoms_\mu\)
Definition: The set of atomic set of valuations with granularity \(\mu\)
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity,

Definition: The set of \(g'\in atoms_\mu\) such that [$]\llbracket{}g'\rrbracket\subseteq\llbracket{}g\rrbracket[/$]
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity,
\(g\in \mathcal G(\mu)\)
Notation: \(atoms_\mu(g)\)

Name: An atomic symbolic alphabet
Definition: An alphabet whose every constraint belongs to \(atoms_\mu\)
Page: 7
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity,

Name: A timed game graph over \(\tilde\Sigma\)
Definition: A deterministic finite state timed transition system over an atomic symbolic alphabet \(\Gamma\) based on \(\Sigma\).
Page: 7
Section: 4
Variables: \(\tilde\Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet
Denoted by: \(\mathcal H\)

Name: A timed game over \(\Gamma\)
Definition: \(\mathcal H\) is a timed game graph over \(\tilde \Sigma\) and
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
Definition2: \(L\subseteq T\Sigma^\omega\) is the winning set
Conjdef: A pair

Name: A play in this game
Definition: Players: \(C\) and \(E\)
Page: 7
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\)
Definition2: State: an element \(\gamma\in\Gamma^*\) and the state \(q\) such that \(q_0\xrightarrow{\gamma} q\)
Conjdef: All of
Definition3: Turn: from a state \(q\), \(C\) chooses a valid subset of symbolic actions enabled at \(q\), player \(E\) responds by choosing an action \(u_0\) from that subset

Name: A valid set of symbolic actions enabled at \(s\)
Definition: deterministic: does not contains two symbolic actions of the form \((a,g,Y)\) and \((a,g,Y')\) with \(Y\ne Y'\)
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
\(\gamma\in L^*_{sym}(\mathcal H)\)
\(s=state_{\mathcal H}(\gamma)\)
Definition2: non-restricting,
Conjdef: A set of symbolic actions enabled at \(s\) which is
Definition3: non-blocking w.r.t. \(\gamma\)
Denoted by: \(U\)

Name: A non-restricting set of symbolic actions enabled at \(s\)
Definition: For each symbolic action of the form \((e,g,Y)\) enabled at \(s\) with \(e\in \Sigma_E\), \(U\) should include an action of the form \((e,g,Y')\) for some \(Y'\) (i.e. same action when the set of reset clocks is not considered).
Page: 7
Section: 4
Variables: \(\tilde\Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
\(\mathcal H\) a timed game graph over \(\tilde\Sigma\),
\(\gamma\in L^*_{sym}(\mathcal H)\)
\(s=state_{\mathcal H}(\gamma)\)
Intuition: every actions that the environment could do, it could still do it, apart that the set of reset clock may change.

Name: A non-blocking set of symbolic actions enabled at \(s\)
Definition: If there exists a symbolic action \((b,g,Y)\) enabled at \(s\) with \(tw(\gamma\cdot (b,g,Y))\ne\emptyset\) then there should exist an action \((c,g',Y')\in U\) such that \(tw(\gamma\cdot (c,g',Y'))\ne\emptyset\).
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) a symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
\(\gamma\in L^*_{sym}(\mathcal H)\)
\(s=state_{\mathcal H}(\gamma)\)
Intuition: deadlock should not be created

Name: A controller with the non-blocking property
Definition: Whenever \(\tau\in L(\mathcal P||\mathcal C)\) and \(\tau\cdot (b,t)\in L(\mathcal P)\), there exists \(c\in\Sigma\) and \(t'>0\) such that \(\tau\cdot(c,t')\in L(\mathcal P||\mathcal C)\).
Page: 5, 5
Section: 3, 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 C\) a timed TS over \((\Sigma,X_{\mathcal P}\cup X_{\mathcal C})\) of granularity \(\mu\)
Name2: Property (C3)
Intuition: Dead-lock can not be created.

Question: Difference between blocking and restricting:
Answer: -Restricting consists in forbidding something to the environment
-Blocking consists in creating a deadlock
Page: 5,7

Name: A stategy for player \(C\)
Definition: this function is defined on \(\epsilon\)
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
Definition2: for each \(\gamma\in\Gamma^*\) in its domain, \(\gamma\cdot u\) for \(u\in f(\gamma)\) also belongs to the domain
Conjdef: such that all of
Definition3: for each \(\gamma\) such that \(f(\gamma)\) is defined, \(f(\gamma)\) is valid at \(state_{\mathcal H}(\gamma)\) w.r.t. \(\gamma\)
DefType: A partial function \(f:\Gamma\to\Gamma^*\)

Name: A play according to \(f\)
Definition: A play \(\gamma\) such that, for every prefix \(\gamma'\cdot u\), \(u\in f(\gamma')\)
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
\(f\) a strategy for player \(C\)

Definition: The set of infinite plays according to \(f\).
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
\(f\) a strategy for player \(C\)
Notation: \(plays_f(\mathcal H)\)

Definition: The set of finite plays according to \(f\).
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
\(\mathcal H\) a timed game graph over \(\tilde \Sigma\),
\(f\) a strategy for player \(C\)
Notation: \(plays^*_f(\mathcal H)\)

Name: A strategy winning for \(C\)
Definition: whose all infinite plays are winning for \(C\)
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \((\mathcal H,L)\) a timed game graph over \(\tilde \Sigma\),
Definition2: \(tw(plays_f(\mathcal H))\) is disjoint from \(L\)
Conjdef: A strategy \(f\), equivalently

Name: A finite state strategy
Definition: A strategy such that there exists a deterministic finite state transition system \(\mathcal T\) over \(\Gamma\), with \(f(\gamma)\) given by the set of actions enabled at \(state_{\mathcal T}(\gamma)\)
Page: 7
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal H\) a timed game graph over \(\tilde \Sigma\),

Definition: set of states \(P\)
Page: 8
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal P=(P,p_0,\rightarrow)\) a plant over \(\tilde\Sigma\),
\(\mathcal C\) a \(\mu\)-controller
\(\mu=(X_{\mathcal P\cup\mathcal C},m,max)\) a granularity
Notation: \(\mathcal H_{\mathcal P,\mu}\)
Definition2: initial state \(p_0\)
Conjdef: The finite state-timed transition system
Definition3: arrows \((q,(a,g',Y\cup Y'),q')\) iff:
-there exists a transition of the form \(q\xrightarrow[Y]{a,g}q'\) in \(\mathcal P\)
-\(g'\in atoms_\mu(g)\) and
-\(Y'\subseteq X_C\)
Definition4: alphabet \(\Sigma\times atoms_\mu\times 2^{X_\mathcal C\cup X_\mathcal P} \)

Smaller0: there exists a (finite-state) \(\mu\)-controller for \(\mathcal P\) which satisfies \(\mathcal A_s\)
Greater0: player \(C\) has a (finite-state) winning startegy in \((\mathcal H_{\mathcal P,\mu},L(\mathcal A_s))\)
Page: 8
Section: 4
Variables: \(\tilde \Sigma=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
\(\Gamma\) an atomic symbolic alphabet based on \(\tilde\Sigma\)
Let \(\mathcal P=(P,p_0,\rightarrow)\) a plant over \(\tilde\Sigma\),
\(\mathcal C\) a \(\mu\)-controller
\(\mu=(X_{\mathcal P\cup\mathcal C},m,max)\) a granularity
\(\mathcal A_s\) a specification of undesirable behaviours
Index: 1
Kind: Lem
Smaller to greater: iff

Name: A state-based game over \(\tilde\Delta\)
Definition: \(\mathcal K\) is a deterministic finite state transition system over \(\Delta\)
Page: 8
Section: 5
Variables: \(\tilde \Delta=(\Sigma_C,\Sigma_E)\) a partitionned alphabet,
Definition2: \(val:Q\to 2^{(2^\Delta)}\) a function that identifiers the valid choices player \(C\) can offer at a state in \(\mathcal K\)
Conjdef: A tuple
Definition3: \(\mathcal F\) a winning condition stated as an acceptance condition on the states of \(\mathcal K\)

Name: A time-successor region of \(r\)
Definition: A region \(r'\) containing a valuation \(v+t\) with \(v\in r\) and \(t>0\).
Page: 8, 177 A tool for deciding the satisfiability of continuous-time metric temporal logic
Section: 5
Variables: \(\mu=(X,m,max)\) a granularity
\(r\) a region of \(\mu\)
\(g\) a \(\mu\)-clock constraint
\(Y\subseteq X\)
Definition2: A region \(r'\) containing a valuation \((v+t)[Y\leftarrow 0]\) with \(v\in r\), \(t>0\) and \(Y\subseteq X\).
Conjdef: Depending on authors

Name: A successor region of \(r\) w.r.t. to \((a,g,Y)\)
Definition: \(r'\) is a time successor region \(r\),
Page: 8
Section: 5
Variables: \(\mu=(X,m,max)\) a granularity
\(A\) an alphabet,
\(\Gamma\) a symbolic alphabet of granularity at most \(\mu\),
\(r\) a region of \(\mu\)
\(g\) a \(\mu\)-clock constraint
\(Y\subseteq X\)
Definition2: \(r'\models g\)
Conjdef: A region \(r'[0/Y]\) such that

Smaller0: \(g\in atoms_\mu\)
Greater0: at most one
Page: 8
Section: 5
Variables: \(\mu=(X,m,max)\) a granularity
\(\Sigma\) an alphabet,
\(a\in\sigma\)
\(\Gamma\) a symbolic alphabet of granularity at most \(\mu\),
\(r\) a region of \(\mu\)
\(g\) a \(\mu\)-clock constraint
\(Y\subseteq X\)
Prefix Smaller: the number of successor region of \(r\) w.r.t. to \((a,g,Y)\) is

Question: The set of words \(\gamma\in\Gamma^\omega\) such that \(tw(\gamma)\) is disjoint from \(L(\mathcal A)\) is
Answer: \(\omega\)-regular
Page: 9
Section: 5
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks
\(\Gamma\) a symbolic alphabet based on \((\Sigma,X)\)
\(\mathcal A\) a timed \(\omega\)-automaton over \((\Sigma,X')\)

Question: The number of \(\subseteq\)-maximal languages accepted by an automaton of granularity at most \(\kappa\), disjoint from \(L(\mathcal A)\) is
Answer: exactly one.
Page: 9
Section: 5
Variables: \(\Sigma\) an alphabet,
\(X\) a set of clocks
\(\kappa\) a granularity
\(\mathcal A\) a timed \(\omega\)-automaton
Index: 1
Kind: Cor

Definition: An automaton recognizing the set of words \(\gamma\in\Gamma^\omega\) such that \(tw(\gamma)\) is disjoint from \(L(A)\)
Page: 9
Section: 5
Variables: \(\tilde\Sigma\) an alphabet,
\(\Gamma\) a symbolic alphabet,
\(\nu\) its granularity,
\(\mathcal A\) a timed \(\omega\)-automaton over \(\Gamma\)
Notation: \(\mathcal B\)
Notation2: \((B,b_0,\to,ind)\)

Definition: \(Q=S\times reg_\nu\times B\)
Page: 9
Section: 5
Variables: \(\tilde\Sigma\) an alphabet,
\(\Gamma\) a symbolic alphabet,
\(\nu\) its granularity,
\(\mathcal A\) a timed \(\omega\)-automaton over \(\Gamma\)
\(\mathcal H=(S,s_0,\delta)\) a timed graph
\(\mathcal B=(B,b_0,\to,ind)\) an \(\omega\)-automaton recognizing the set of words \(\gamma\in\Gamma^\omega\) such that \(tw(\gamma)\) is disjoint from \(L(A)\)
\(\Delta_C\) and \(\Delta_E\) being the set of \((a,g,Y)\in\Delta\) with \(a\in \sigma C\) or \(\Sigma_E\)
Notation: \(\Phi\)
Definition2: \(q_0=(s_0,[\mathbf 0],b_0)\)
Conjdef: \((\mathcal K=(Q,q_0,\delta'),val,ind')\) over \(\tilde\Delta\)with
Definition3: \(\delta'((s,r,b),(a,g,Y))\) being the 3-tuple:
-\(\delta(s,(a,g,Y))\),
-a successor of \(r\) with respect to \((a,g,Y)\)
-a successor of \(b\) by \((a,g,Y)\) in \(\mathcal B\)
Definition4: \(val(q)\) is the set of actions \(U\) enabled at \(q\) such that:
-\(U\) is deterministic,
-\(U\) is non restricting at \(q\) w.r.t. \(\tilde\Sigma\),
-\(U\) is non-blocking
Definition5: \(ind'((s,r,b))=ind(b)\)

Smaller0: Player \(C\) has a (finite state) winning strategy in the timed game \(\Omega=(\mathcal H,L(\mathcal A))\)
Greater0: Player \(C\) has a (finite state) winning strategy in the classical game graph \(\Phi\)
Page: 9
Section: 5
Variables: \(\tilde\Sigma\) an alphabet,
\(\Gamma\) a symbolic alphabet,
\(\nu\) its granularity,
\(\mathcal A\) a timed \(\omega\)-automaton over \(\Gamma\)
\(\mathcal H=(S,s_0,\delta)\) a timed graph
\(\mathcal B=(B,b_0,\to,ind)\) an \(\omega\)-automaton recognizing the set of words \(\gamma\in\Gamma^\omega\) such that \(tw(\gamma)\) is disjoint from \(L(A)\)
\(\Delta_C\) and \(\Delta_E\) being the set of \((a,g,Y)\in\Delta\) with \(a\in \sigma C\) or \(\Sigma_E\)
Index: 3
Kind: Lem
Smaller to greater: iff

Name: Its set of prefix
Page: 3
Section: 2
Variables: \(A\) an alphabet,
\(\alpha\in A^\infty\)
Abbreviation: \(pre(\alpha)\)

Name: Deterministic timed transitions
Page: 5
Section: 2
Under: synchronized product

Name: The set of regions, according to granularity \(\mu\)
Page: 6
Section: 4
Variables: \(\mu=(X,m,max)\) a granularity,
Abbreviation: \(reg_\mu\)