Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / A theory of timed automata
Tags: closed fromAlgorithm fromMath hasNotNewEffectReturnsMeaning hasSeenConjDef mathToSee // autDone defToAut stateInitialClockTransitionFinal typToBinary

Name: Discrete time model
Definition: A model in which each time is an integer greater than the preceding time.
Page: 3
Chapter: 1

Question: What to do with discrete-time words ?
Answer: Transform it into an usual non-timed words, where the i-th letter is the letter associated to time i if it exists, and a special symbol silent otherwise
Page: 3
Chapter: 1

Name: Fictitious-clock model
Definition: The list of time is a non-decreasing sequence of integer, representing the floor of the real time.
Page: 3
Chapter: 1

Question: What to do with fictitious-clock words ?
Answer: Transform it into an usual non-timed words, adding a tick symbol each time the time is incremented.
Page: 4
Chapter: 1

Name: Dense-time model
Definition: The sequence of time is an increasing sequence of real
Page: 186
Chapter: 1
Extra: Dense because values are real: a dense set

Question: Difference between monotically and monoticity ?
Answer: Monoticity is increasing, monotically is non-decreasing
Page: 191
Chapter: 3
Section: 1

Smaller0: monotically
Greater0: monoticity
Page: 191
Chapter: 3
Section: 1
Hide sides: ye

Name: Untime
Definition: \((\sigma_i,\tau_i)_{i\in\mathbb N}\mapsto (\sigma_i)_{i\in\mathbb N}\) with \(\sigma_i\in\Sigma\), \(\tau_i\in\mathbb R\)
Page: 191
Chapter: 3
Section: 1
Kind: Def

Name: Timed regular languages
Page: 197
Section: 6
Chapter: 3
Index: 15
Kind: Theo
Under: union
Condition: finite
Under2: intersection

Page: 197
Implementation: \(\langle\Sigma,\bigcup_i S_i,\bigcup_i S_{io},\bigcup_iC_i,\bigcup_iE_i,\bigcup_iF_i\rangle\)
Section: 6
Chapter: 3
Effect: A TBA accepting the union of the languages of \(\mathcal A_i\)
Variables: \(\mathcal A_i=\langle \Sigma,S_i,S_{io},C_i,E_i,F_i\rangle\) TBA
Index: 15
Kind: Theo

Page: 197
Variables: \(\mathcal A_i=\langle \Sigma,S_i,S_{i,0},C_i,E_i,F_i\rangle\) TBA for \(1\le i\le n\)
Section: 6
Chapter: 3
Transitions: \(E(\langle s_1,\dots, s_n,j\rangle,a,\langle s'_1,\dots,s'_n,j'\rangle)\) with \(E_i(s_i,a,s'_i)\), and \(j'\) being \(j+1\) if \(s_j\in F_j\), and being \(j\) otherwise. I.e. it simulates transition in each automata, and the counter is incremented when an accepting state is met.
States: \(S=\Pi_{i=1}^nS_i\times \{1,\dots,n\}\) a state being a tuple of states from each automaton and a counter
Initial: \(S_0=\Pi_{i=1}^nS_{i,0}\times\{1\}\) an initial state is a union of state, with counter starting at 1
Name: A TBA accepting the intersections of the languages of \(\mathcal A_i\)
Final: \(F=\Pi_{i=1}^{n-1}S_i\times F_n\times \{n\}\) i.e. the counter is at \(n\) and the \(n\)-th state is final (thus counter will be incremented on next move)
Clock number: \(C=\bigcup_{i=1}^nC_i\) the disjoint union of clocks

Question: Assume that semantic is restrained to rational time, then
Answer: \(Untime[L(\mathcal A)]\) remains unchanged
Page: 197
Chapter: 3
Section: 6
Variables: \(\mathcal A=\langle \Sigma,S,S_{i},C,E,F\rangle\) TBA

Definition: A TBA, similar to \(\mathcal A\), with each real in clock constraints multiplied by \(t\)
Page: 200
Chapter: 4
Section: 1
Variables: \(t\in\mathbb Q\),
\(\mathcal A=\langle \Sigma,S,S_{i},C,E,F\rangle\) TBA
Notation: \(\mathcal A_t\)
Kind: Lem

Smaller0: \((\bar s,\bar v)\) is a run of \(\mathcal A\) over \((\sigma,\tau)\)
Greater0: \((\bar s,t\cdot\bar v)\) is a run of \(\mathcal A_t\) over \((\sigma,t\cdot \tau)\)
Page: 200
Chapter: 4
Section: 1
Variables: \(t\in\mathbb Q\),
Let \(\mathcal A=\langle \Sigma,S,S_{i},C,E,F\rangle\) a timed transition table,
\((\sigma,\tau)\) a timed word
Kind: Lem
Smaller to greater: iff

Question: How to transform \(\mathcal A\) in an TBA with integer constants, such that both or none are empty ?
Answer: Takes \(\mathcal A_t\) with \(t\) the lcm of the denominators of constants of \(\mathcal A\)
Page: 201
Chapter: 4
Section: 1
Variables: \(\mathcal A=\langle \Sigma,S,S_{i},C,E,F\rangle\) TBA
Kind: Lem

Name: An extended state
Definition: A pair containing an element of \(S\) and a clock interpretation for \(C\)
Page: 201
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Kind: Def
Extra: check name
Denoted by: \(\langle s,v\rangle\)

Definition: The largest integer \(c\) such that \(x\le c\) or \(x\ge c\) is a subformula fo some clock constraint appearing in \(E\)
Page: 202
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
\(c\in C\)
Notation: \(c_x\)
Kind: Def

Definition: For each \(x\in C\), \(\lfloor v_i(x)\rfloor\) are both equal or both greater than \(c_x\),
Page: 202
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
\(v_1,v_2\) clocks interpretations of \(C\)
Notation: \(v_1\sim v_2\)
Index: 3
Kind: Def
Definition2: For each \(x_1,x_2\in C\), with \(v_1(x_j)\le c_{x_j}\), either both \(fract(v_i(x_1))\le fract(v_i(x_2))\) holds or none hold.
Conjdef: All of
Definition3: For each \(x\in C\), with \(v_1(x)\le c_{x}\), either both \(fract(v_i(x_1))\) equals 0 or both are positive.

Definition: The class region of \(v\)
Page: 202
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Let \(v\) clocks interpretations of \(C\)
Notation: \([v]\)
Kind: Def

Name: A clock region
Definition: An \(\sim\)-equivalent class of clock interpretations.
Page: 202
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Let \(v\) clocks interpretations of \(C\)
Kind: Def

Question: The number of clock region is
Answer: at most \(|C|!2^{|C|}\Pi_{x\in C}(2c_x+2)\)
Page: 203
Chapter: 4
Section: 2
Variables: \(\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Index: 5
Kind: Lem

Name: The region automaton of \(\mathcal A\)
Definition: State: an element of \(S\) and a clock region
Page: 203, 204
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Notation: \(R(\mathcal A)\)
Index: 8
Kind: Def
Definition2: Initial states: \(\langle s_0,[x\mapsto 0]\rangle\) with \(s_0\in S_0\)
Conjdef: A tuple
Definition3: Transitions: \(\langle \langle s,\alpha\rangle,\langle s',\alpha'\rangle,a\rangle\) iff there is \(\langle s,s',a,\lambda,\delta\rangle\in E\), a region \(\alpha''\) such that \(\alpha''\) is a time successor of \(\alpha\), \(\alpha''\models \delta\) and \(\alpha=[\lambda\mapsto 0]\alpha''\)

Name: A successor of \(\alpha\)
Definition: A clock region \(\alpha'\) such that for each \(v\in\alpha\) there exists a positive \(t\in\mathbb R\) such that \(v+t\in \alpha'\)
Page: 203
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
\(\alpha\) a clock region
Typ: Transitive relation

Question: A clock region is characterized by
Answer: For every clock \(x\), one constraints \(x=c\), \(x>c_x\) or \(c-1<x<c\)
Page: 202
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table
Answer2: for each \(x_1,x_2\) distinct such that \(c_i-1<x_i<c_i\) occurs in the preceding case, we have either \(x_1=x_2\) or \(x_i<x_j\)

Smaller0: for each \(x\in C\), \(\alpha(x)>c_x\)
Greater0: the only time-successor of \(\alpha\) is \(\alpha\)
Page: 204
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
\(\alpha\) a clock region of \(C\)

Smaller0: there exists \(x\in C\) such that \(\alpha(x)=c\) for some \(c\le c_x\)
Greater0: the successors of \(\beta\), where \(\beta\) is similar to \(\alpha\), aparts that \(c<\beta(x)<c+1\) for each \(\alpha(x)=c<c_x\), and \(c_x<\beta(x)\) for each \(\alpha(x)=c_x\)
Page: 204
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
\(\alpha\) a clock region of \(C\)
Prefix Greater: the successors of \(\alpha\) are

Smaller0: there exists no \(x\in C\) such that \(\alpha(x)=c\) for some \(c\le c_x\)
Greater0: \(\beta\) and its successors, where \(\beta\) is similar to \(\alpha\), aparts that \(\beta(x)=c+1\) for each \(c-1<\alpha(x)<c\) with \(frac(\alpha(x))\) maximal, and that constraints involving \(fract(x)\) are removed
Page: 204
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
\(\alpha\) a clock region of \(C\)
Prefix Greater: the successors of \(\alpha\) are

Question: Computing the region graph takes time
Answer: \(O[(|S|+|E|)2^{|\delta(\mathcal A)|}]\).
Page: 205
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
Extra: todo

Definition: \(r:\langle s_1,[v_1]\rangle\xrightarrow{\sigma_1}\langle s_2,[v_2]\rangle\xrightarrow{\sigma_2}\dots\)
Page: 206
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
\(r:\langle s_1,v_1\rangle\xrightarrow[\tau_1]{\sigma_1}\langle s_2,v_2\rangle\xrightarrow[\tau_2]{\sigma_2}\dots\)
Notation: \([r]\)
Index: 10
Kind: Def
Typ: A progressive run of the region automaton

Name: A progressive run of the region automaton
Definition: A run \(r:\langle s_1,\alpha_1\rangle\xrightarrow{\sigma_1}\langle s_2,\alpha_2\rangle\xrightarrow{\sigma_2}\dots\) such that, for each clock \(x\), there is an infinite number of \(\alpha_i\) such that \(\alpha_i(x)\) is either 0 or greater than \(c_x\)
Page: 206
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
Index: 11
Kind: Def

Smaller0: admits a progressive run
Greater0: \(\mathcal A\) admits a run
Page: 206
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
Index: 13
Kind: Lem
Prefix Smaller: \(R(\mathcal A)\)

Smaller0: \(r\) is progessive
Greater0: \(\mathcal A\) admits a run \(r'\) such that \(r=[r']\)
Page: 206
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,
\(r\) a run in \(\mathcal A\)
Index: 13
Kind: Lem

Name: A linear bounded automaton
Definition: A NTM whose tape head can't go beyond the end of the input markers
Page: 209
Chapter: 4
Section: 5

Name: Regular timed languages
Page: 215
Section: 1
Chapter: 5
Index: 6
Kind: Cor
Not: not
Under: complementation

Question: Universality of timed-automata with continuous semantic is
Answer: \(\Pi_1^1\)-hard
Page: 211
Chapter: 5
Section: 2
Kind: Theo

Question: Computing the region graph takes time
Answer: \(O[(|S|+|E|)2^{|\delta(\mathcal A)|}]\).
Page: 205
Chapter: 4
Section: 3
Variables: \(\mathcal A=\langle\Sigma,S,S_0,C,E\rangle\) a timed transition table,