Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Real Time synthesize is hard!
Tags: hasSeenConjDef fromMath fromImplication mulitpledeck

Name: (Finite) timed word over \(\Sigma\)
Definition: A word over \(\Sigma\times \mathbb R^+\), with the real non-decreasing non-negative
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet

Name: The set of (Finite) timed word over \(\Sigma\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Notation: \(T\Sigma^*\)

Name: A timed language
Definition: A subset of \(T\Sigma^*\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2

Name: Metric Temporal Logic
Definition: \(\phi:=\top\mid a\mid\phi\land \phi\mid\neg\phi\mid\phi\mathcal U_I\phi\) with \(a\in\Sigma\) and \(I\) a real interval of non-negative reals
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Abbreviation: MTL

Name: Until operator
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\sigma=(\sigma_1,\tau_1)\dots(\sigma_n,\tau_n)\in T\Sigma^*\),
\(1\le i\le n\),
\(\phi_1,\phi_2\in MTL\)
Notation: \(\mathcal U_I\)

Definition: There exists \(j>i\), such that \((\sigma,j)\models\phi_2\) (i.e. [$]\norm{w_{i..j}}\in I[/$], \(\tau_j-\tau_i\in I\) and \((\sigma,k)\models\phi_1\) for all \(i<k<j\))
Page: 3, 4
Chapter: Real Time synthesize is hard, The compound interest in relaxing punctality
Section: 2, 2
Variables: \(\sigma=(\sigma_1,\tau_1)\dots(\sigma_n,\tau_n)\in T\Sigma^*\),
\(1\le i\le n\),
\(\phi_1,\phi_2\in MTL\)
Notation: \((\sigma,i)\models\phi_1\mathcal U_I\phi_2\)

Name: The next operator
Definition: \(\bot \bigcup_I\phi\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\phi\in MTL\)
Notation: \(\bigcirc _I\phi\)

Name: Finally
Definition: \(\top U_I\phi\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\phi\in MTL\)
Notation: \(\lozenge _I\phi\)

Name: Globally
Definition: \(\neg\lozenge_I\neg\phi\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\phi\in MTL\)
Notation: \(\square_I\phi\)

Name: Dual until
Definition: \(\neg((\neg\phi_1)\bigcup_I(\neg\phi_2))\)
Page: 3
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\phi_1,\phi_2\in MTL\)
Notation: \(\phi_1\tilde\bigcup_I\phi_2\)
Name2: Release
Notation2: \(\phi_1\mathcal R_I\phi_2\)

Name: non-strict until
Definition: \(\phi_2\lor(\phi_1\land\phi_1\bigcup_I\phi_2)\) if \(0\in I\),
\(\phi_1\land\phi_1\bigcup_I\phi_2\) otherwise
Page: 3,4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\phi_1,\phi_2\in MTL\)
Notation: \(\phi_1\overline \bigcup_I\phi_2\)

Definition: A modal operator whose interval is \(\mathbb R^+=[0,\infty)\)
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Denoted by: Omitting subscript of a modal operator

Name: Metric Interval Temporal Logic
Definition: Restriction of MTL to non-singular intervals
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Abbreviation: MITL

Definition: each \(\mathbf U_I\), \(I\) is right-open, and either left open or \(\text{inf}I=0\)
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Notation: Open MITL
Definition2: each \(\mathbf R_I\), \(I\) is closed
Conjdef: both
DefType: The restriction of MITL such that in negation normal form,

Definition: The negation of a formula in open MITL
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Notation: A formula in closed MITL

Definition: A formula in MTL whose negation normal form has all intervals \(\mathrm U_I\) bounded
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Notation: A formula in safety MTL

Definition: in each subformula \(\phi_1\bigcup_I\phi_2\), if \(I\) is unbounded then \(\phi_2\in LTL\),
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Notation: A formula in coFLAT-MTL
Definition2: in each subformulas \(\phi_1\tilde\bigcup_I\phi_2\), if \(I\) is unbounded then \(\phi_1\in LTL\).
Conjdef: The formula satisfies the following in negation normal form

Definition: The restriction of \(L\) to formulas with non-strict variants of the operators
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(L\) a logic included in \(MTL\)
Notation: \(L^{ns}\)

Definition: The restriction of \(L\) in which all intervals are either unbounded or have a left endpoint equal to 0
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(L\) a logic included in \(MTL\)
Notation: \(L[U_{0,\infty}]\)

Definition: The restriction of \(L\) in which, for all \(\lozenge_I\) and \(\square_I\), \(I\) is unbounded.
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(L\) a logic included in \(MTL\)
Notation: \(L[\lozenge_\infty]\)

Name: The set of clock constraints over \(X\)
Definition: containing \(\top\)
Page: 4, 3, 678
Chapter: Real Time synthesize is hard, The compound interest in relaxing punctality, 9 Principles of model checking
Section: 2, 2, 1
Variables: \(X\) a finite set of variables called clocks
Notation: \(\mathcal G(X)\)
Index: , , 2
Kind: ,, Def
Definition2: closed under conjunctions
Conjdef: The least set
Definition3: containing \(x\sim c\) with \(\sim\in\{<,\le,=,\ge,>\}\), \(x\in X\) and \(c\in\mathbb Q^+\)
Notation2: \(\Phi(X)\)

Name: A valuation over \(X\)
Definition: A mapping \(\nu:X\to\mathbb R^+\)
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(X\) a finite set of variables called clocks

Definition: The valuation \(x\mapsto \nu(x)+r\)
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(X\) a finite set of variables called clocks,
\(\nu\) a valuation over \(X\),
\(r\in\mathbb R^+\)
Notation: \(\nu+r\)

Definition: The valuation \(x\mapsto 0\) if \(x\in R\) and \(x\mapsto \nu (x)\) otherwise
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(X\) a finite set of variables called clocks,
\(\nu\) a valuation over \(X\),
\(R\subseteq\mathbb X\)
Notation: \(\nu[R\leftarrow 0]\)

Name: A granularity
Definition: \(X\) a finite set of variables called clocks
Page: 4
Chapter: Real Time synthesize is hard
Section: 2
Definition2: \(m\in\mathbb N\setminus\{0\}\),
Conjdef: \((X,m,K)\) with
Definition3: \(K\in\mathbb N\)

Name: A \(\mu\)-granular constraint
Definition: A constraint such that each constant in \(g\) is of the form \(\frac\alpha m\) with \(\alpha\le K\) integral
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mu=(X,m,K)\) a granularity

Name: A symbolic alphabet based on \((\Sigma,X)\)
Definition: A finite subset of \(\Sigma\times\mathcal G^{atom}_{m,K}(X)\times 2^X\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks
Name2: A \((X,m,K)\)-granular symbolic alphabet based on \((\Sigma,X)\)

Definition: the set of atomic \((X,m,K)\)-granular clock constraints
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks
Notation: \(\mathcal G^{atom}_{m,K}(X)\)

Name: An atomic \((X,m,K)\)-granular clock constraints
Definition: A \((X,m,K)\)-granular clock constraints \(g\) such that [$]\llbracket g\rrbracket[/$] is included into, or disjoint from, each \((X,m,K)\)-granular clock constraints \(g'\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks,
\(m\in\mathbb N\setminus\{0\}\),
\(K\in\mathbb N\)
Extra: seems to not be the correct definition

Name: A symbolic word
Definition: A word over the symbolic alphabets
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks,
\(m\in\mathbb N\setminus\{0\}\),
\(K\in\mathbb N\)

Name: The set of timed words over \(\Sigma\) generated by \(\gamma\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks,
\(m\in\mathbb N\setminus\{0\}\),
\(K\in\mathbb N\)
\(\gamma=(\sigma_1,g_1,R_1)\dots(\sigma_n,g_n,R_n)\) a symbolic ord over \(\Gamma\)
Notation: \(tw(\gamma)\)

Name: The intuition of \((\sigma_i,g_i,R_i)\)
Definition: Action \(\sigma_i\) is performed, \(g_i\) satisfied and \(R_i\) reset
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks,
\(m\in\mathbb N\setminus\{0\}\),
\(K\in\mathbb N\)
\(\gamma=(\sigma_1,g_1,R_1)\dots(\sigma_n,g_n,R_n)\) a symbolic word over \(\Gamma\)

Name: Symbolic transition system based on \((\Sigma,X)\)
Definition: \(S\) a set of locations,
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet
Definition2: \(s_0\in S\) the initial location,
Conjdef: A tuple with
Definition3: \(\Delta\subseteq S\times\Gamma\times S\) the transition relation
Abbreviation: STS
Definition4: \(S_f\subseteq S\) a set of accepting locations (omitted if all locations are accepting)
Denoted by: \(\mathcal T\)

Name: A timed automaton
Definition: An STS with finitely many locations
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Abbreviation: TA

Name: A path in \(\mathcal T\)
Definition: An element \(\pi=s_1\xrightarrow{b_1}s_2\xrightarrow{b_2}\dots\xrightarrow{b_n}s_{n+1}\) with \((s_i,b_i,s_{i+1})\in \Delta\) for all \(1\le i\le n\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\)

Name: The trace of \(\pi\)
Definition: the word \(b_1\dots b_n\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
\(\pi=s_1\xrightarrow{b_1}s_2\xrightarrow{b_2}\dots\xrightarrow{b_n}s_{n+1}\) a path in \(\mathcal T\)

Name: An accepting path in \(\mathcal T\)
Definition: \(\pi=s_1\xrightarrow{b_1}s_2\xrightarrow{b_2}\dots\xrightarrow{b_n}s_{n+1}\) a path in \(\mathcal T\) such that \(s_{n+1}\in \Sigma_f\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),

Definition: The language of \(\mathcal T\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
Notation: \(\mathcal L(\mathcal T)\)

Name: A word accepted by \(\mathcal T\)
Definition: A trace of a finite accepting paths starting in \(s_0\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),

Name: A timed action enabled in \(\mathcal T\) at a pair \((s,\nu)\)
Definition: A timed action \((t,\sigma)\) such that there exists a transition \((s,(\sigma,g,R),s')\in \Delta\) such that \(\nu+t\models g\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
\(\nu\) a valuation,
\(s\in S\)

Name: The set of timed action enabled in \(\mathcal T\) at \((s,\nu)\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
\(\nu\) a valuation,
\(s\in S\)
Notation: \(\text{En}_{\mathcal T}(s,\nu)\)

Name: A time deterministic STS
Definition: An STS \(\mathcal T=(S,s_0,\Delta,S_f)\) such that there are no distinct transitions \((s,(\sigma,g_1,R_1),s_1)\) and \((s,(\sigma,g_2,R_2),s_2)\) in \(\Delta\) such that there exists a valuation \(\nu\) such that \(\nu\models g_1\) and \(\nu\models g_2\).
Page: 5
Chapter: Real Time synthesize is hard
Section: 2

Smaller0: \(\mathcal T\) is time deteministic
Greater0: there is at most one path whose trace \(\gamma\) verifies \(\sigma\in tw(\gamma)\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
\(\sigma\) a timed word
Extra: multiple if

Definition: The unique pair, if it exists, reached after reading \(\sigma\in tw(\gamma)\)
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Gamma\) a symbolic alphabet,
\(X\) a set of clock,
\(\Sigma\) a finite alphabet,
\(\mathcal T=(S,s_0,\Delta,S_f)\) a Symbolic transition system based on \((\Sigma,X)\),
\(\sigma\) a timed word
Notation: \(\delta(s_0,\sigma)\)
Assuming: \(\mathcal T\) time deterministic

Name: The set of controllable actions
Page: 5
Chapter: Real Time synthesize is hard
Variables: \(\Sigma\) an alphabet
Notation: \(\Sigma_C\)

Name: The set of environment actions
Page: 5
Chapter: Real Time synthesize is hard
Variables: \(\Sigma\) an alphabet
Notation: \(\Sigma_E\)

Name: A reactive synthesis family of problems
Definition: state: timed words
Page: 6
Chapter: Real Time synthesize is hard
Section: 2
Definition2: initial state: the empty timed word,
Conjdef: A game with
Definition3: controller proposes potentially a timed action \((t,a)\in \mathbb R^+\times \Sigma_C\), the environment proposes a timed word \((t',b)\in \mathbb R^+\times \Sigma_E\), firable in the plant, the least timed action is added to the word. In case of equality, non-deterministic choice is made
Abbreviation: RS

Definition: A specification \(S\in\mathcal F\),
a plant \(\mathcal P\), which are interpreted over elements of \(T\Sigma^b\).
The timed language is represented as desired or undesired behavior depending on \(s\)
Page: 6
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathcal F\) a fragment of MITL,
\(s\in\{u,d\}\),
\(b\in\{\star,\omega\}\)
Notation: \(RS^b_s(\mathcal F)\)

Name: A timed words over \(\Sigma\) generated by \(\gamma\)
Definition: A \((\sigma_1,\tau_1)\dots(\sigma_n,\tau_n)\) such that there is a sequence \((\nu_i)_{0\le i\le n}\) of valuations with \(\nu_0\) the zero valuation, and for all \(1\le i\le n\), \(v_{i-1}+\tau_i-\tau_{i-1}\models g_i\)and \(\nu_i=(\nu_{i-1}+\tau _i-\tau_{i-1})[R_i\leftarrow 0]\) (assuming \(\tau_0=0\))
Page: 5
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\Sigma\) a finite alphabet,
\(X\) a finite set of clocks,
\(m\in\mathbb N\setminus\{0\}\),
\(K\in\mathbb N\)
\(\gamma=(\sigma_1,g_1,R_1)\dots(\sigma_n,g_n,R_n)\) a symbolic ord over \(\Gamma\)

Name: The set of valuations over \(X\) which satisfy \(g\)
Page: 3, 4
Chapter: Timed Control Synthesis for External Specifications,
Real time synthesis is hard
Section: 2, 2
Variables: \(X\) a set of clocks,
\(g\) a constraint
Notation: [$]\llbracket{}g \rrbracket_X[/$]
Notation2: [$]\llbracket{}g \rrbracket[/$]

Name: the set of timed words consistent with \(\mathcal T\) and \(\mathcal P\)
Definition: containing the empty timed word,
Page: 7
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathcal T=(S,s_0,\delta)\) an STS,
\(\mathcal P\) a plant
Notation: \(T\Sigma^*_{\mathcal {T,P}}\)
Definition2: for each elements, it contains its possible successor according to what the controller can play
Conjdef: The least subset of \((\Sigma\times \mathbb R)^+\)
Definition3: closed under successor of word

Name: A \(\mathfrak L\) bounded-resources synthesis problem
Definition: A problem both in \(\text{BPrecRS}^\star_d(\mathfrak L)\) and in \(\text{BClockRS}^\star_d(\mathfrak L)\).
Page: 7
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathfrak L\) a fragment of \(MTL\)
Abbreviation: \(\text{BResRS}^\star_d(\mathfrak L)\)

Name: \(\mathfrak L\) bounded precision synthesis problem
Definition: The restriction of \(\mathbf{IRS}_d^\star(\mathfrak L)\) where the precision of the controller is fixed
Page: 7
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathfrak L\) a fragment of \(MTL\)
Notation: \(\text{BPrecRS}^\star_d(\mathfrak L)\)

Name: \(\mathfrak L\) bounded-clocks synthesis problem
Definition: The restriction of \(\mathbf{IRS}_d^\star(\mathfrak L)\) where the number of clock of the controller is fixed
Page: 8
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathfrak L\) a fragment of \(MTL\)
Abbreviation: \(\text{BClocksRS}^\star_d(\mathfrak L)\)

Name: A deterministic channel machine
Definition: \(S\) a finite set of states
Page: 8, 6
Chapter: Real Time synthesize is hard,
Controller Synthesis for MTL Specifications
Section: 3, 3
Definition2: \(s_0\in S\) the initial state
Conjdef: A tuple with
Definition3: \(\Delta\subseteq S\times\{m!,m?\mid m\in M\}\times S\) such that, for each \(s\in S\), either there is a single transition with \(!\) or there is at most one transition for each \(m?\) with \(m\in M\)
Abbreviation: DCM
Definition4: \(M\) a finite set of messages
Denoted by: \(\mathcal S\)
Definition5: \(s_{halt}\) the halting state

Name: time unit
Page: 9
Section: 3
Abbreviation: t.u.

Definition: An environment move stating that the read action of the controller was not legal
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(Check^\leftarrow\)

Definition: An environment move stating that the write action of the controller was not legal
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(Check^\rightarrow\)

Definition: Only legal play after the end of the encoding
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(Nil_C\), \(Nil_E\)

Definition: A move controlled by the environment stating that it loses
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(Lose\)

Definition: An action controlled by the controller, stating that it wins
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(Wins\)

Definition: \(S\cup\{Check^\leftarrow,Check^\rightarrow,Lose,Nil_E\}\)
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(\Sigma_E\) for the encoding of \(\mathcal S\)

Definition: \(\{m!,m?\mid m\in M\}\cup\{Win,Nil_C\}\)
Page: 10
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Notation: \(\Sigma_C\) for the encoding of \(\mathcal S\)

Question: \(RS^\star_d(MITL)\) is
Answer: undecidable
Page: 11
Section: 3
Index: 1
Kind: Theo

Question: \(RS^b_s(L)\) is
Answer: undecidable
Page: 12
Section: 3
Variables: \(s\{u,d\}\),
\(b\in\{\star,\omega\}\)
\(L\in\{Open-MITL^{ns}[\lozenge_\infty], Closed-MITL^{ns}[\lozenge_\infty]\}\)
Index: 2
Kind: Theo

Question: \(RS^b_s(L)\) is
Answer: undecidable
Page: 12
Section: 3
Variables: \(s\{u,d\}\),
\(b\in\{\star,\omega\}\)
\(L\in\{Safety-MTL,coFlat-MTL\}\)
Kind: Theo

Definition: closed under finite conjunction and disjunction,
Page: 20
Section: E
Variables: \(\Sigma\) an alphabet
Notation: \(\Gamma(L)\)
Definition2: containing \(y.\gamma\) with \(y\) the unique clock
Conjdef: The least set of formulas
Definition3: Containing \(y\sim c\), \(y\) the unique clock, \(c\in\mathbb N\) and \(\sim\in\{<,\le,=,>,\ge\}\)
Definition4: Containing \(\bot\) and \(\top\)
Definition5: Containing elements of \(L\)

Definition: Reset the clock \(y\) and execute \(\gamma\)
Page: 20
Section: E
Variables: In OCATA,
\(x\) a clock
\(\gamma\in \gamma(L)\)
Notation: \(y.\gamma\)

Definition: Execute non deterministically \(\gamma\) and \(\gamma'\)
Page: 20
Section: E
Variables: In OCATA
Context: Label of edges over OCATA
Notation: \(\gamma\land\gamma'\)
Extra: gamma ?

Name: A configuration in classical semantic
Definition: A set of states in classical semantic
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA

Name: A state in classical semantic
Definition: The pair containing a location and a clock valuation
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA
Context: OCATA

Question: The size of its equivalent OCATA in classical semantic
Answer: is linear in the number of subformulas
Page: 13
Section: 4
Variables: \(\phi\in MTL\)
Extra: Classical semantic ?

Name: An execution in classical semantic
Definition: A sequence of configuration of classical semantic
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA

Name: A configuration in interval semantic
Definition: A set of states in interval semantic
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA

Name: A state in interval semantic
Definition: The pair containing a location and an interval for the clock
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA
Context: Ocata

Name: An execution in interval semantic
Definition: A sequence of configuration of classical semantic
Page: 13
Section: 4
Variables: \(\Sigma\) an alphabet
\(\mathcal A=(L,\ell_0,\delta,L_f)\) an OCATA

Definition: An element of \(\Gamma\).
Page: 5
Chapter: Real-Time synthesis is hard
Variables: \(\Gamma\) a symbolic alphabet
\(STS\) an STS based on \((\Sigma,X)\)
Intuition: A transition of the STS
Denoted by: \(b_i\)

Question: What can the controller play ?
Answer: -\((t,b)\), with \(b\in\Sigma_C\) and \((t,b)\) fireable in controller and plant after having read \(\sigma(c,T)\).
-Or nothing
Page: 7
Chapter: Real time syntfehsis is hard
Section: 4
Variables: \(\mathcal T=(S,s_0,\delta)\) an STS,
\(\mathcal P\) a plant,
\(\sigma(c,T)\) a state in the RS problem,

Question: What is the following state when controller plays \((t,b)\)
Answer: either:
-\(\sigma(c,T)(b,T+t)\), or
-\(\sigma(c,T)(a,T+t')\), with \(t'\le t\), \((t',a)\) fireable in plant and controller and \(a\in\Sigma_E\)
Page: 7
Chapter: Real time syntfehsis is hard
Variables: \(\mathcal T=(S,s_0,\delta)\) an STS,
\(\mathcal P\) a plant,
\(\sigma(c,T)\) a state in the RS problem,
\((t,b)\) fireable in controller and plant after having read \(\sigma(c,t)\)

Name: The encoding of the maximal correct path as a timed word
Definition: \(Nil_C\) is a special action of the controller
Page: 9
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Definition2: \((s_i,a_i,s_{i+1})\in\Delta\),
Conjdef: A play of the form \(Nil_C^*s_0a_0s_1a_1\dots\), where
Definition3: \(s_i\) comes with no delay,
Definition4: \(a_i\) comes with a delay
Definition5: write and read comes in pair, separated by 1 time unit, apart may be for write at the last time unit

Name: The possible maximal path in \(\mathcal S\)
Definition: A path reaching \(s_{halt}\)
Page: 9
Section: 3
Variables: \(\mathcal S=(S,s_0,s_{halt},M,\Delta)\) a Deterministic Channel Machine in normal form
Definition2: an infinite path
Definition3: a blocking path, where the head of the channel can not be read by the last state

Name: One-clock alternating timed automaton over \(\Sigma\)
Definition: \(L\) a finite set of locations,
Page: 20
Section: E
Variables: \(\Sigma\) an alphabet
Definition2: \(\ell_0\in L\) the initial location
Conjdef: A tuple with
Definition3: \(L_f\subseteq L\) its set of final locations
Abbreviation: OCATA over \(\Sigma\)
Extra: \(\Gamma\) is a set of formula defined in another note
Definition4: \(\delta:L\times \Sigma\to\Gamma(L)\)

Name: \(\mathfrak L\) implementable reactive synthesis problem
Definition: Deciding, given a plant \(\mathcal P\) and a specifiaction given as an \(\mathfrak L\) formula \(\phi\), whether there exists a set of clocks, a symbolic alphabet and a time-deterministic STS such that \(T\Sigma^\star_{\mathcal{T,P}}\cap \mathcal L(\mathcal P)\subseteq \mathcal L(\phi)\cup\{\epsilon\}\)
Page: 7
Chapter: Real Time synthesize is hard
Section: 2
Variables: \(\mathfrak L\) a fragment of \(MTL\)
Abbreviation: \(\mathbf{IRS}_d^\star(\mathfrak L)\)