Title: Theory / Unimportant / CS / Softw / UPPAAL / Main
Tags: récupéré MissingMedia hasSeenConjDef seen_description defToType hasNotNewEffectReturnsMeaning

Name: A timed automaton
Definition: \(N\) is a finite set of locations/nodes
Page: 3
Section: 2.1
Index: 1
Kind: Def
Definition2: \(l_0\in N\) the initial location
Conjdef: A tuple
Definition3: \(E\subseteq N\times\mathcal{B}(C)\times \Sigma\times 2^{\mathcal C}\times N\) the set of edges
Definition4: \(I:N\to\mathcal B(C)\) assigns invariants to locations
Denoted by: \(\mathcal A\)

Name: the set of clocks
Page: 3
Section: 2.1
Notation: \(\mathcal C\)
Index: 1
Kind: Def

Name: A clock
Page: 3
Section: 2.1
Index: 1
Kind: Def
Denoted by: \(x,y,\dots\)

Name: A finite alphabet
Page: 3
Section: 2.1
Notation: \(\Sigma\)
Index: 1
Kind: Def
Conjdef: A tuple
Denoted by: \(a,b,\dots\)

Definition: The set of clock constraints, ranged over by \(g\) and also by \(D\)
Page: 3
Section: 2.1
Variables: \(\mathcal C\) a clock
Notation: \(\mathcal{B(C)}\)

Definition: \(\langle l,g,a,r,l'\rangle\in E\)
Page: 3
Section: 2.1
Variables: \(\mathcal A=(N,l_0,E,I)\)
Notation: \(l\xrightarrow{g,a,r}l'\)

Name: A state
Definition: A state of \(N\)
Page: 4
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
Definition2: A clock assignment
Conjdef: A tuple with

Name: Operational semantic
Definition: \(\langle l,u+d\rangle\) if \(u,u+d\in I(l)\) for \(d\ge 0\)
Page: 4
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(\mathcal A=(N,l_0,E,I)\)
\(\langle l,u\rangle\) a state
Definition2: \(\langle l',u'\rangle\) if \(l\xrightarrow{g,a,r}l'\), \(u\in g\), \(u'=[r\mapsto 0]u\) and \(u\in I(l')\)
Conjdef: The semantic such that the successors of \(\langle l,u\rangle\) are

Name: A timed action
Definition: An element of \(\mathbb R_+\times\Sigma\)
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
Denoted by: \((t,a)\)

Name: The time-stamp of the action \(a\)
Definition: \(t\)
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
\((t,a)\) a timed action

Name: A timed trace
Definition: A sequence of timed action with non-decreasing time-stamps.
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(\mathcal A=(N,l_0,E,I)\)
Denoted by: \(\xi\)

Name: A run of \(\mathcal A\) over \(\xi\)
Definition: A sequence of transitions \(\langle l_0,u_0\rangle\xrightarrow{d_1}\xrightarrow{a_1}\langle l_2,u_2\rangle\xrightarrow{d_2}\xrightarrow{a_2}\dots\) with \(t_i=t_{i-1}+d_i\) for all \(i\in\mathbb N\)
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
\(\xi=(t_i,a_i)_{i\in\mathbb N}\)
Index: 3
Kind: Def

Name: The untimed language of \(\mathcal A\)
Definition: The set of all traces in the form \(a_1\dots \) for which there exists a timed trace \((t_1,a_1)\dots\) in the timed language of \(\mathcal A\).
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
Notation: \(L_{untimed}(\mathcal A)\)
Index: 3
Kind: Def

Name: A bisimulation over the states of timed transition systems and the alphabet \(\Sigma\cup\mathbb R_{+}\)
Definition: for all \((s_1,s_2)\in R\), \(s_1\xrightarrow{\sigma}s'_1\) for some \(\sigma\in \Sigma\cup\mathbb R_+\) and \(s'_1\), then \(s_2\xrightarrow{s'_2}\) and \(s'_1,s'_2)\) for some \(s'_2\)
Page: 5
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
Index: 4
Kind: Def
Conjdef: A symmetrical binary relation satisfying
Denoted by: \(R\)

Name: Timed bisimilar automaton
Definition: Two timed automaton such that there is a bisimulation containing the initial states of the automata
Page: 6
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet

Definition: \(\langle l,u\rangle\xrightarrow {\sigma}\langle l',u'\rangle\) for some \(\sigma\in\Sigma\cup\mathbb R_+\)
Page: 6
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
\(l\in N\), \(u\) a valuation over \(\mathcal C\)
Notation: \(\langle l,u\rangle\to\langle l',u'\rangle\)
Index: 5
Kind: Def

Name: A reachable state
Definition: A state \(\langle l,u\rangle\) such that \(\langle l_0,u_0\rangle\to^*\langle l,u\rangle\)
Page: 6
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
\(u_0\) the initial clock valuation
Index: 5
Kind: Def

Name: \(\langle l,\phi\rangle\) is reachable
Definition: \(\langle l_0,u_0\rangle\to^*\langle l,u\rangle\) for \(u\) satisfying \(\phi\)
Page: 6
Section: 2.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(\mathcal A=(N,l_0,E,I)\)
\(\phi\in\mathcal {B(C)}\)
\(l\in L\)
Index: 5
Kind: Def

Name: The clock ceiling
Definition: A function of type \(\mathcal C\to\mathbb N\)
Page: 6
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
Kind: Def
Denoted by: \(k\)

Definition: \(\lfloor u(x)\rfloor = \lfloor v(x)\rfloor\) or (\(u(x)>k(x)\) and \(v(x)>k(x)\))
Page: 6
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(k\) a clock ceiling
\(u,v\) two clocks valuation
Notation: \(u\dot\sim_k v\)
Kind: Def
Definition2: \(u(x)\le k(x)\) implies \(\{u(x)\}=0\) iff \(\{v(x)\}=0\)
Conjdef: for all \(x,y\in \mathbb C\)
Definition3: (\(u(x)\le k(x)\) and \(v(x)\le k(x)\)) implies \(\{u(x)\}\le \{u(y)\}\) iff \(\{v(x)\}\le\{v(y)\}\)

Definition: \(\dot\sim_k\) with \(k\) the greatest constant used in \(\mathcal A\)
Page: 6
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\)
\(u,v\) clock valuations
Notation: \(u\dot \sim v\)
Kind: Def

Name: A clock region
Definition: An equivalence class of clock valuation under \(\dot\sim_k\)
Page: 6
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(k\) a clock ceiling
Kind: Def

Name: The region graph of \(\mathcal A\)
Definition: A state is a location of \(N\) and a region for the clocks
Page: 7
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(\mathcal A=(N,l_0,E,I)\) a timed automaton
Index: 6
Kind: Def
Definition2: Initial state \(\langle l_0,[\mathbf 0]\rangle\)
Conjdef: An automaton with
Definition3: \(\langle l,[u]\rangle\implies \langle l',[u']\rangle\) for \(\langle l',u\rangle\xrightarrow d\langle l,u'\rangle\) for \(d\in\mathbb R^{>0}\cup\Sigma\)
Name2: The region automaton of \(\mathcal A\)

Name: A zone
Typ: A clock constraint
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clock
Kind: Def

Definition: The maximal set of clock assignments satisfying \(D\)
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clock
Let \(D\) a zone
Notation: \([D]\)
Kind: Def

Definition: The set of zones of \(\mathcal C\)
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clock
Notation: \(\mathcal{B(C)}\)
Kind: Def

Name: A symbolic state
Definition: An element of \(N\times\mathcal{B(C)}\)
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
Kind: Def

Definition: The set of \(u+d\), with \(u\in D\) and \(d\in\mathbb R_+\)
Page: 8, 22
Section: 3.1, 4.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Notation: \(D^\uparrow\)
Notation2: up(D)

Definition: the set of \([r\mapsto 0]u\) with \(u\in D\)
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Notation: \(r(D)\)
Notation2: reset(D,r:=0)

Definition: to \(\langle l,D^\uparrow\land I(l)\rangle\)
Page: 8
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Notation: \(\rightsquigarrow\)
Definition2: to \(\langle l',r(D\land g)\land I(l')\rangle\) if \(l\xrightarrow{g,a,r}l'\)
Conjdef: The relation over symbolic states, associating \(\langle l,D\rangle\)

Name: A zone closed under entailment
Definition: A zone such that no constraint can be added without reducing the solution set
Page: 9
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
Abbreviation: A zone closed

Smaller0: \(\langle l_0,\{u_0\}\rangle\rightsquigarrow\langle l_f,D_f\rangle\)
Greater0: \(\langle l_0,u_0\rangle\rightarrow^*\langle l_f,u_f\rangle\) for all \(u_f\in D_f\)
Page: 9
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
\(l_0\in N\)
\(u_0\) a clock valuation
Name: Soundness

Smaller0: \(\langle l_0,\{u_0\}\rangle\rightsquigarrow^*_k\langle l_f,D_f\rangle\)
Page: 11
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
\(l_0\in N\)
\(u_0\) a clock valuation
Index: 2
Kind: Theo
Smaller to greater: \(\langle l_0,u_0\rangle\rightarrow^*\langle l_f,u_f\rangle\) for all \(u_f\in D_f\) such that \(u_f(x)\le k(x)\) for all \(x\)
Name: Soundness

Smaller0: \(\langle l_0,u_0\rangle\rightarrow^*\langle l_f,u_f\rangle\) with \(u_f(x)\le k(x)\) for all \(x\)
Page: 11
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
\(l_0\in N\)
\(u_0\) a clock valuation
Index: 2
Kind: Theo
Smaller to greater: \(\langle l_0,\{u_0\}\rangle\rightsquigarrow_k^*\langle l_f,D_f\rangle\) for some \(D_f\ni u_f\)
Smaller1: there are no guards of the form \(x-y\sim n\)
Name: Soundness

Smaller0: \(\langle l_0,u_0\rangle\rightarrow^*\langle l_f,u_f\rangle\)
Greater0: \(\langle l_0,\{u_0\}\rangle\rightsquigarrow\langle l_f,D_f\rangle\) for some \(D_f\ni u_f\)
Page: 9
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
\(l_0\in N\)
\(u_0\) a clock valuation
Name: Completeness

Name: A diagonal free automaton
Definition: An automaton whose guard does not compare pair of clocks
Page: 10
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet

Definition: The set of \(u\) such that \(u\dot\sim_{k,\mathcal G} v\) for \(v\in D\)
Page: 13, 24-25
Section: 3.1, 4.3
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(D\) a zone
\(k\) a clock ceiling
Notation: \(norm_{k,\mathcal G}(D)\)
Index: 10
Kind: Def
Definition2: The union of \(\mathrm{norm}_k(D)\land\neg\mathcal G_{unsat}\bigwedge_{g\in G}g\land \bigwedge_{g\in\mathcal G\setminus(\mathcal G_{unsat}\cup G)}\neg g\), for \(G\subseteq \mathcal G\setminus\mathcal G_{unsat}\)
Notation2: \([D]_k\)
Property: Not neccesarily convex
Cardinal: A finite set of equivalence classes,

Definition: The set of \(u\) such that \(u\dot\sim _k v\) for \(v\in D\)
Page: 10, 24
Section: 3.1, 4.3
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(D\) a zone
\(k\) a clock ceiling
Notation: \(norm_k(D)\)
Index: 8
Kind: Def
Definition2: The zone obtained from \(D\) by removing all constraints of the form \(x<m\), \(x\le m\), \(x-y\le m\), \(x-y\le m\) where \(m>k(x)\).
replacing \(m\) by \(k(x)\) in the constraints of the form\(x>m\), \(x\ge m\), \(x-y>m\), \(x-y\ge m\) where \(m>k(x)\).
Put back in normal form
Denoted by: \([D]_k\)

Question: The number of normalized zone is
Answer: finite.
Page: 10
Section: 3.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(k\) a clock ceiling
Index: 8
Kind: Def

Definition: \(u\dot\sim_kv\)
Page: 13
Section: 3.3
Variables: \(\mathcal C\) a set of clocks,
\(\mathcal G\) a finite set of difference constarints of the form \(x-y\sim n\), for \(x,y\in\mathcal C\), \(\sim\in\{\le,<,=,>,\ge\}\), \(n\in\mathbb N\)
\(k\) for a clock ceiling
Notation: \(\dot\sim_{k,\mathcal G}\)
Index: 10
Kind: Def
Definition2: for all \(g\in\mathcal G\), \(u\in g\) iff \(v\in g\)
Conjdef: The relation on pair \((u,v)\) of valuations with

Definition: The relation containing \(\langle l,D\rangle,\langle l',norm_{k,\mathcal G}(D')\rangle\) for each \(\langle l,D\rangle\rightsquigarrow\langle l',D'\rangle\)
Page: 13
Section: 3.3
Variables: \(\mathcal C\) a set of clocks,
\(\mathcal G\) a finite set of difference constarints of the form \(x-y\sim n\), for \(x,y\in\mathcal C\), \(\sim\in\{\le,<,=,>,\ge\}\), \(n\in\mathbb N\)
\(k\) for a clock ceiling
Notation: \(\rightsquigarrow_{k,\mathcal G}\)
Index: 10
Kind: Def

Page: 14
Section: 3.4
Notation: Whether \(\langle l_f,\phi_f\rangle\) is reachable
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
Let \(\mathcal A=(N,l_0,E,I)\) a timed-automaton
\(l_f\in N\),
\(\phi_f\in \mathcal{D(C)}\)
\(k\) a clock ceiling
\(\mathcal G\) a set of comparisons
Kind: Algo
Index: 1
Context: \(\phi_f\) and the guards respects the clock ceiling \(k\) and its comparisons belong to \(\mathcal G\)

Page: 15,16
Implementation: A matrix \(\mathcal C_0\times\mathcal C_0\) with the \((c,c')\)-th element representing the constraint \(c-c'\le n\), or \(\infty\) if there are no such constraint
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
Name: Difference bound matrices
Index: 1
Kind: Algo
Abbreviation: DBM
Invariant: \(M(D)_{\mathbf 0,c}=0\)
Abstract data structure: A clock constraint

Definition: \(\mathcal C\cup\{\mathbf 0\}\)
Page: 14
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
Notation: \(\mathcal C_0\)
Index: 1
Kind: Algo

Question: Representation of \(x\sim m\) in \(\mathcal C_0\)
Answer: \(x-\mathbf 0\sim n\)
Page: 14
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
Index: 1
Kind: Algo

Name: The order on the elements of \(M(D)\)
Definition: \((n,\preceq)<\infty\)
Page: 16
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone,
\(\preceq\) being \(\le\) or \(<\)
Definition2: \((n_1,\preceq_1)<(n_2,\preceq_2)\) if \(n_1<n_2\)
Conjdef: The relation containing
Definition3: \((n,<)<(n,\leq)\)

Name: The addition on the elements of \(M(D)\)
Definition: \((n,\preceq)+\infty=\infty\)
Page: 16
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone,
\(\preceq\) being \(\le\) or \(<\)
Definition2: \((m,\leq)+(n,\leq)=(m+n,\leq)\)
Conjdef: The relation containing
Definition3: \((m,<)+(n,\prec)=(m+n,<)\)

Name: The graph associated to \(M\)
Definition: nodes being element of \(\mathcal C_0\)
Page: 16
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
Definition2: An edge \((c,(n,\preceq),c')\) for \((n,\preceq)\in M_{c,c'}\)
Conjdef: The digraph with

Page: 17
Section: 4.1
Notation: A canonical matrix equivalent to \(M\)
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
Example: Transform \(M\) into a digraph, apply Floyd-Warshall algorithm, transform back into a DBM

Name: The closure of \(M\)
Definition: The shortest path between all clocks
Page: 17
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM

Name: A zero cycle
Definition: A cycle whose sum of weight is 0
Page: 18
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
\(G\) its graph

Name: A redundant edge
Definition: An edge \((c,n_{c,c'},c')\) such that there is another path between \(c\) and \(c'\) where the sum of weights is no larger than \(n_{c,c'}\)
Page: 18
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
\(G\) its graph

Page: 19, 36
Section: 4.1, appendix
Notation: The equivalent graph constraint without redundant constraint
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
\(G\) its graph
Example: Partition the nodes according to 0 path. Choosing a representatives in each class.
Apply the algorithm for graph without zero-cycle, removing the edges between two non-representatives of distinct classes.
Context: \(G\) in shortest path form

Page: 18, 35
Section: 4.1, Appendix
Notation: The equivalent graph constraint without redundant constraint
Variables: \(\mathcal C\) a set of clocks,
\(M\) a DBM
\(G\) its graph
Example: For each \(c,c',c''\), consider whether \(n_{c,c'}+n_{c',c''}\le n_{c,c''}\), in this case, remove \(n_{c,c''}\)
Context: No zero cycle
\(G\) in shortest path form

Page: 21
Section: 4.1
Notation: Whether the set is consistent
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Example: Check wether \(D_{0,0}<0\)
Context: Set of clocks
Intuition: \(consistent(D)\)
Assuming: \(D\) in canonical form

Page: 21
Section: 4.1
Notation: Whether the set is consistent
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Example: Check whether an upper bound is set to lower value than the corresponding lower bound.
Intuition: \(consistent(D)\)

Page: 18, 36
Section: 4.1, Appendix
Notation: Whether \(D\subseteq D'\)
Variables: \(\mathcal C\) a set of clocks,
\(D,D'\) zones
Example: Whether for each \(c,c'\in\mathcal C\), \(D_{c,c'}\le D_{c,c'}'\)
Kind: Algo
Index: 5
Intuition: \(relation(D,D')\)

Page: 22
Section: 4.1
Notation: The zone satisfying both the constraints of \(D\) and \(x_c-c_{c'}\preceq b\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) zones
\(c,c'\in\mathcal C\)
\(b\in\mathbb N\)
Example: If \((b,\preceq)<D_{c,c'}\), set \(D_{c,c'}\) to \((b,\preceq)\) and put back in canonical form, using Floyd-Warshall restricted to \(c\) and \(c'\).
Intuition: \(and(D,x_c-c_{c'}\preceq b)\)

Page: 18
Section: 4.1
Notation: whether \(x_c-c_{c'}\preceq m\) and \(D\) are consistent
Variables: \(\mathcal C\) a set of clocks,
\(D\) zones
\(c,c'\in\mathcal C\)
\(m\in\mathbb N\)
Example: Whether setting \(D_{c,c'}\) to \(m\) would create a negative cycle. On canonical form, whether \((m,\preceq)+D_{ji}\) is negative
Intuition: \(satisfied(D,x_c-c_{c'}\preceq m)\)

Name: A canonical DBM
Definition: A BDM such that no atomic constraint can be strengthened without losing solutions. With \(D {0,0}<0\) if an upper bound is greater than a lower bound.
Page: 16
Section: 4.1

Page: 22
Section: 3.1, 4.1
Notation: \(UP(D)\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
Example: \(D\) without the upper bound on individual clocks

Definition: The set of \(u[x=d]\) for \(u\in D\) and \(d\ge0\)
Page: 23
Section: 4.1
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(c\in\mathcal C\)
Notation: \(free(D,c)\)
Definition2: Set \(D_{0,c}\) to \((0,\le)\)
Set \(D_{c',c}\) to \(D_{c',0}\)
Remove the constraints \(D_{c,c'}\)
Applied to3: \(D\) without constraints of the clock \(x\)

Definition: The set of \(g\in\mathcal G\) such that \(g\land D=\emptyset\) and of \(\neg g\in\mathcal G\) such that \(\neg g\land D=\emptyset\)
Page: 24
Section: 4.3
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(c\in\mathcal C\)
\(m\in\mathbb Z\)
Notation: \(\mathcal G_{unsat}\)

Meaning: A difference constraint between two clocks
Page: 24
Section: 4.3
Variables: \(\mathcal C\) a set of clocks,
Value: Max int for \(\infty\)
least significant bit being 1 for non-strict order, 0 for strict order. The integer value in the remaining of the memory word
Extra: no information loss with computation->variable transfer.

Question: How to store a DBM ?
Answer: Row by row if the number of clock is known
Layer by layer if clock should be added during a run
Page: 24
Section: 4.3
Variables: \(\mathcal C\) a set of clocks,

Name: Row wise representation of a matrix
Definition: \((x,y)\mapsto x(n+1)+y\)
Page: 28
Section: 4.4
Variables: \(n\in\mathbb N\)

Name: Layered representation of a matrix
Definition: \((x,y)\mapsto \left\{\begin{array}{ll}y(y+1)+x&\text{ if $x\le y$}\\x^2+y&\text{otherwise}\end{array}\right.\)
Page: 27, 28
Section: 4.4
Variables: \(n\in\mathbb N\)

Name: A process
Definition: A timed automaton in a network
Page: 29
Section: 5.1
Context: UPPAAL

Name: Action alphabet
Page: 29
Section: 5.1
Context: UPPAAL
Notation: \(\Sigma\)
Typ: A set of symbols, with \(?a\) iff there is \(!a\)

Name: An input action
Page: 29
Section: 5.1
Context: UPPAAL
Notation: \(a?\)

Name: An output action
Page: 29
Section: 5.1
Context: UPPAAL
Notation: \(a!\)

Name: An internal action
Page: 29
Section: 5.1
Context: UPPAAL
Notation: \(\tau\)

Name: The CCS parallel composition of the \(A_i\)'s
Definition: Set of locations is \(\prod N_i\)
Page: 29
Section: 5.1
Variables: \(\mathcal C\) a set of clocks,
\(\Sigma\) a finite alphabet
\(\mathcal A_i=(N_i,l_{0,i},E_i,I_i)\) timed-automaton
Context: UPPAAL
Notation: \(A_1\mid \dots\mid A_n\)
Definition2: Initial location \((l_{0,1},\dots,l_{0,n})\)
Conjdef: The timed automaton
Definition3: Invariant \(I(l_1,\dots, l_n)=\bigwedge I_i(l_i)\)
Definition4: A transition \(\langle l,u\rangle\xrightarrow d\langle l,u+t\rangle\) if \(u\in I(l)\) and \((u+d)\in I(l)\)
Definition5: A transition \(\langle l,u\rangle\xrightarrow \tau\langle l[l'_i/l_i],[r\mapsto 0]u\rangle\) if \(l_i\xrightarrow{g,\tau,r}l'_i\), \(u\in g\), \([r\mapsto 0]u\in I(l[l'_i/l_i])\)
Definition6: A transition \(\langle l,u\rangle\xrightarrow \tau\langle l[l'_i/l_i][l'_j/l_j],[r_i\cup r_j\mapsto 0]u\rangle\) if there exists \(i\ne j\) such that \(l_i\xrightarrow{g,a?,r}l'_i\) \(l_j\xrightarrow{g,a!,r}l'_j\), \(u\in g\), \([r_i\cup r_j\mapsto 0]u\in I(l[l'_i/l_i][l'_j/l_j])\)

Name: Urgent channel
Definition: A channel such that, if it is enabled, the system may not take a delay transition.
Page: 30
Section: 5.1
Assuming: There are no clock guard on edges synchronizing with such a channel

Name: Committed location
Definition: A location where no delay is allowed
Page: 32
Section: 5.1

Instruction: A[]\(\phi\)
Page: 32
Effect: Invariently \(\phi\)
Section: 5.2
Variables: \(\phi\) a TCTL formula

Instruction: A<>\(\phi\)
Page: 32
Effect: Always Eventually \(\phi\)
Section: 5.2
Variables: \(\phi\) a TCTL formula

Instruction: E<>\(\phi\)
Page: 32
Effect: Possibly \(\phi\)
Section: 5.2
Variables: \(\phi\) a TCTL formula

Instruction: E[]\(\phi\)
Page: 32
Effect: Potentially Always \(\phi\)
Section: 5.2
Variables: \(\phi\) a TCTL formula

Instruction: \(\phi -->\psi\)
Page: 32
Effect: \(A[](\phi\implies A<>\psi)\)
Section: 5.2
Variables: \(\phi,\psi\) a TCTL formula
Intuition: \(\phi\) always leads to \(\psi\)

Page: 35
Section: Appendix
Variables: \(D\) a DBM
Kind: Algo
Index: 2
Intuition: \(\texttt{close}(D)\)

Page: 22, 37
Section: 4.1, Appendix
Notation: \(down(D)\)
Variables: \(D\) a DBM
Name: the set of \(u\) such that \(u+d\in D\) for some \(d\ge 0\)
Example: The zone, similar to \(D\), except that the lower bound for \(c\) is the minimum bound on \(c'-c\) found in DBM
Kind: Algo
Index: 7

Page: 22, 37
Section: 4.1, Appendix
Variables: \(D\) a DBM
\(c\) a clock
Kind: Algo
Index: 8
Intuition: \(and(D,c)\)

Page: 23, 38
Section: 4.1, Appendix
Notation: The set of \(u[c=n]\) for \(u\in D\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(c\in\mathcal C\)
\(m\in\mathbb N\)
Example: \(D\), with \(D_{c,0}=(m,\le)\) and \(D_{0,c}=(-m,\le )\)
Kind: Algo
Index: 10
Intuition: \(reset(D,c:=m)[/$

Page: 23, 38
Section: 4.1, Appendix
Notation: The set of \(u[c=u(c')]\) for \(u\in D\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(c,c'\in\mathcal C\)
\(m\in\mathbb N\)
Example: Setting \(D_{c,c''}\) to \(D_{c',c''}\) and similarly for \(c'\) in second position, for all \(c''\)
Kind: Algo
Index: 11
Intuition: \(copy(D,c:=c')\)

Page: 23, 38
Section: 4.1, Appendix
Notation: The set of \(u[c=u(c)+m]\) for \(u\in D\)
Variables: \(\mathcal C\) a set of clocks
\(D\) a zone
\(c\in\mathcal C\)
\(m\in\mathbb N\)
Example: Adding \(m\) to the lower and upper bound related to \(c\)
Kind: Algo
Index: 12
Intuition: \(shift(D,c:=c+m)\)

Page: 39
Section: Appendix
Notation: Core normalization of \(D\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(k\) a clock ceiling
Kind: Algo
Index: 14
Intuition: Core-Norm_k(D)

Page: 39
Section: Appendix
Notation: Zone splitting of \(D\)
Variables: \(\mathcal C\) a set of clocks,
\(D\) a zone
\(\mathcal G_d\) a set of comparison constraint
Kind: Algo
Index: 15
Intuition: split(D)

Page: 39
Section: Appendix
Notation: \(b_1+b_2\)
Variables: \(b_1,b_2\) encoded bounds
Kind: Algo
Index: 17
Commutative: UPPAAL

Name: A difference constraint between two clocks
Typ: Max int for \(\infty\)
least significant bit being 1 for non-strict order, 0 for strict order. The integer value in the remaining of the memory word
Page: 24
Section: 4.3