Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 09 - Timed Automata
Tags: fromImplication hasSeenConjDef fromRelation autDone defToAut toAutomata
On every note of this deck, unless a note says otherwise:
Chapter: 9

Name: \(\bigcirc^k\)
Definition: Empty word if \(k=0\),
\(\bigcirc^{k-1}\bigcirc\) otherwise
Page: 674
Variables: \(k\in\mathbb N\)

Name: A clock
Definition: Intuitively, a stopwatch, which can be checked and restarted
Page: 677
Section: 1

Definition: The set of clock constraints over \(C\)
Page: 678
Section: 1
Variables: \(C\) a set of clock
Notation: \(CC(C)\)
Index: 2
Kind: Def

Name: An atomic clock constraint
Definition: A clock constraint without conjunctions
Page: 678
Section: 1
Variables: \(C\) a set of clock
Index: 2
Kind: Def

Name: The set of all atomic clock constraints over \(C\)
Page: 678
Section: 1
Variables: \(C\) a set of clock
Index: 2
Kind: Def
Abbreviation: \(ACC(C)\)

Name: A timed automaton
Definition: \(Loc\) a finite set of locations
Page: 678
Section: 1
Index: 3
Kind: Def
Definition2: \(Act\) a finite set of actions,
Conjdef: A tuple with
Definition3: \(Loc_0\subseteq Loc\) a set of initial locations,
Definition4: \(C\) a finite set of clocks
Denoted by: \(TA\)
Definition5: \(\hookrightarrow\subseteq Loc\times CC(C)\times Act\times 2^C\times Loc\) a transition relation
Definition6: \(Inv:Loc\to CC(C)\) an invariant assignement function
Definition7: \(AP\) a finite set of atomic propositions and
-\(L:Loc \to 2^{AP}\) is a labeling function for the locations

Definition: The set of atomic clock constraint that occur in guards or in location invariant of \(TA\)
Section: 1
Variables: \(TA\) a timed automaton
Notation: \(ACC(TA)\)
Index: 3
Kind: Def

Page: 679
Section: 1
Notation: [$]l\xhookrightarrow {g:\alpha,D}l'[/$]
Intuition: The TA can move from \(l\) to \(l'\), if the clock constraint \(g\) holds. In this case, clocks in \(D\) will be reset to \(0\) and \(\alpha\) is performed

Definition: The amount of time the automaton can spend in \(l\)
Page: 679
Section: 1
Variables: \(TA\) a TA,
\(l\) a location
Notation: \(Inv(l)\)

Name: The handshaking of \(TA_1\) and \(TA_2\)
Definition: \(Loc_1\times Loc_2\)
Similar to the one of other system,
Invariant of \((l1,l2)\) are the union of the invariants of \(l_i\),
A transition from \((l1,l2)\) is guarded by the conjonction of the transitions from the \(l_i\)s
Page: 683
Section: 1
Variables: \(TA_1,TA_2\) TAs,
\(H\) actions commons to to the two TAs
Notation: \(TA_1||_HTA_2\)
Definition2: \(Act_1\cup Act_2\), \(C_1\cup C_2\)
Conjdef: The TA
Definition3: [$]\frac{\ell_1\xhookrightarrow{g_1:\alpha,D_1}\ell'_1\land\ell_2\xhookrightarrow{g_2:\alpha,D_2}\ell'_2}{\langle\ell_1,\ell_2\rangle\xhookrightarrow{g_1:\alpha,D_1}\langle\ell'_1,\ell'_2\rangle}[/$] for \(\alpha\in H\)
[$]\frac{\ell_1\xhookrightarrow{g_1:\alpha,D_1}\ell'_1}{\langle\ell_1,\ell_2\rangle\xhookrightarrow{g_1:\alpha,D_1}\langle\ell'_1,\ell_2\rangle}[/$] for \(\alpha\not\in H\)
[$]\frac{\ell_2\xhookrightarrow{g_2:\alpha,D_2}\ell'_2}{\langle\ell_1,\ell_2\rangle\xhookrightarrow{g_1:\alpha,D_1}\langle\ell_1,\ell'_2\rangle}[/$] for \(\alpha\not\in H\)
Extra: union ?
Definition4: \(Loc_{0,1}\cup Loc_{0,2}\)
Definition5: \(Inv(\langle \ell_1,\ell_2\rangle)=Inv_1(\ell_1)\land Inv_2(\ell_2)\)
Definition6: \(AP_1\cup AP_2\)
Definition7: \(L(\langle \ell_1,\ell_2\rangle)=L_1(\ell_1)\land Inv_2(\ell_2)\)

Name: A clock valuation for \(C\)
Definition: A function \(C\to \mathbb R_{\ge 0}\)
Page: 686
Section: 1.1
Variables: \(C\) a set of clock
Kind: Def
Denoted by: \(\eta\)

Definition: The set of all clock valuations over \(C\)
Page: 686
Section: 1.1
Variables: \(C\) a set of clock
Notation: \(Eval(C)\)
Kind: Def

Definition: The clock valuation of \(\{x_i\}\) with \(x_i\mapsto v_i\)
Page: 686
Section: 1.1
Variables: \((v)_{i=1}^n\in\mathbb R_{\ge0}\)
Notation: \([x_1=v_1,\dots, x_n=v_n]\)

Definition: Defined as usual by induction on the clock constraint's syntax. Atomic propositions are straightforward
Page: 687
Section: 1.1
Variables: \(C\) a set of clocks,
\(\eta\in Eval(C)\),
and \(g\in CC(C)\)
Notation: \(\eta\models g\)
Index: 10
Kind: Def

Definition: \(x_i\mapsto \eta(x_i)+d\)
Page: 687
Section: 1.1
Variables: \(C\) a set of clocks,
\(\eta\in Eval(C)\),
and \(d\in\mathbb R_{\ge0}\)
Notation: \(\eta+d\)
Index: 10
Kind: Def

Definition: \(x\mapsto 0\) and \(y\mapsto\eta(y)\) for each \(y\in C\setminus \{x\}\)
Page: 687
Section: 1.1
Variables: \(C\) a set of clocks,
\(\eta\in Eval(C)\),
and \(x\in C\)
Notation: reset \(x\) in \(\eta\)
Index: 10
Kind: Def

Name: A discrete transition
Definition: Taking a transition in the timed automaton
Page: 687
Section: 1.1
Variables: \(A\) a TA
Index: 10
Kind: Def

Name: A delay transition
Definition: Letting time progress while staying in a location
Page: 687
Section: 1.1
Variables: \(A\) a TA
Index: 10
Kind: Def

Page: 687
Variables: \(TA=(Loc,Act,C,\hookrightarrow, Loc_0,Inv,AP,L)\) a timed automaton
Section: 1.1
Chapter: 9
Transitions: \((l,\eta)\xrightarrow\alpha(l',\eta')\) if
--there is a transition [$]l\xhookrightarrow{g:\alpha,D} l'\in TA[/$],
--\(\eta\models g\)
--\(\eta'=reset D\) in \(\eta\)
--\(\eta'\models Inv(l')\)
- and \((l,\eta)\xrightarrow{d}(l,\eta+d)\) for \(d\in\mathbb R_{\ge 0}\) if \(\eta+d\models Inv(l)\)
States: \(S=Loc\times Eval(C)\)
Initial: \(I=\{(l_0,\eta)\mid l_0\in Loc_0\land \eta(x)=0\text{ for all }x\in C\}\),
Notation: \(TS(TA)\)
Alphabet: \(AP'=AP\cup ACC(C)\)
Kind: Def
Index: 10
Typ: The TS
Labeling function: \(L'(l,\eta)=L(l)\cup\{g\in ACC(C)\mid \eta\models g\}\),
Actions: \(Act'=Act\cup\mathbb R_{\ge 0}\),

Question: the analysis of timed automata is focused on
Answer: time-divergent paths
Page: 691
Chapter: 9
Section: 1.2

Definition: [$]\defFun{(Act\cup\mathbb R_{>0})}{\mathbb R_{\ge 0}}{\begin{array}{ll}\tau\in Act\\d\in\mathbb R_{>0}\end{array}}{\left\{\begin{array}{ll}0\\d\end{array}\right.}[/$]
Page: 691
Section: 1.2
Variables: \(TA\) a TA
Notation: ExecTime
Index: 15
Kind: Def

Definition: \(\sum \tau_i \)
Page: 691
Section: 1.2
Variables: \(TA\) a TA,
\(\rho\) an execution fragment with transitions \(\tau _i\)
Notation: \(ExecTime(\rho)\)
Index: 15
Kind: Def

Definition: \(ExecTime(\rho)\) where \(\rho\) induces \(\pi\)
Page: 691
Section: 1.2
Variables: \(TA\) a TA,
\(\pi\) a path fragment in \(TS(TA)\)
Notation: \(ExecTime(\pi)\)
Index: 15
Kind: Def

Name: A divergent path fragment
Definition: A path fragment \(\pi\) such that \(ExecTime(\pi)=\infty\)
Page: 692
Section: 1.2
Variables: \(TA\) a TA,
Index: 16
Kind: Def

Name: A convergent path fragment
Definition: A path fragment \(\pi\) such that \(ExecTime(\pi)\in\mathbb R\)
Page: 692
Section: 1.2
Variables: \(TA\) a TA,
Index: 16
Kind: Def

Definition: \(\{\pi\in Paths(s)\mid \pi\text{ is time divergent}\}\)
Page: 692
Section: 1.2
Variables: \(TA\) a TA,
\(s\in TS(TA)\)
Notation: \(Paths_{div}(s)\)
Index: 18
Kind: Def

Definition: A state \(s\) such that \(Path_{div}(s)=\emptyset\)
Page: 692
Section: 1.2
Variables: \(TA\) a TA,
Notation: A state which contains a timelock
Index: 19
Kind: Def

Definition: A TA such that no state of \(Reach(TS(TA))\) contains a timelock
Page: 692
Section: 1.2
Notation: A timelock-free TA
Index: 18
Kind: Def

Question: Difference between terminal state and terminal location
Answer: A terminal state belongs to a TS and means no progress can be made
A terminal location belongs to a TA, and it may be possible to spend infinitely many time in it
Page: 693
Chapter: 9
Section: 1.2
Index: 18
Kind: Def

Name: A zeno path
Definition: time-convergent
Page: 694
Section: 1.2
Variables: \(TA\) a TA
Index: 22
Kind: Def
Definition2: with infinitely many actions belonging to \(Act\)
Conjdef: A path

Name: A non-zeno TA
Definition: A TA \(TA\) without initial zeno path in \(TS(TA)\)
Page: 694
Section: 1.2
Index: 22
Kind: Def

Question: How can a non-zeno TA possess zeno path
Answer: The path starts in unreachable state
Page: 694
Chapter: 9
Section: 1.2
Index: 22
Kind: Def

Smaller0: for every control cycle in \(TA\), [$]\ell_0\xhookrightarrow{g_1:\alpha_1,C_1}\ell_1\xhookrightarrow{g_2:\alpha_2,C_2}\dots\xhookrightarrow{g_n:\alpha_n,C_n}\ell_n[/$] with \(\ell_0=\ell_n\), there exists a clock \(x\in C\) such that
Greater0: \(TA\) is non-zeno
Page: 695, 696
Chapter: 9
Section: 1.2
Variables: \(TA\) a TA,
\(C\) its set of clocks
Smaller2: \(x\in C_i\) for some \(0<i\le n\)
Smaller3: for all clock evaluations \(\eta\) there exists \(c\in\mathbb N_{>0}\) such that \(\eta(x)<c\) implies (\(\eta\not\models g_j\) or \(Inv(\ell_j)\)) for some \(0<j\le n\)

Smaller0: \(\pi\) is zeno
Greater0: \(\pi\) is time-convergent
Page: 694
Chapter: 9
Section: 1.2
Variables: \(TA\) a TA, with set \(C\) of clocks,
\(\pi\) a path

Definition: the equivalence class containing all infinite path fragments induced by execution fragments in \(TS(TA)\) of the form
\(s_0\xrightarrow{d_0^1}\dots\xrightarrow{d_0^{k_0}}s_0+d_0\xrightarrow{\alpha_0}s_1\dots \) with \(\sum_{j=1}^{k_0} s_{i}^{j}=d_0\)
Page: 697
Section: 1.2
Variables: \(TA\) a TA,
\((d_i)_{i\in\mathbb N}\)
Notation: [$]s_0\xRightarrow{d_0}s_1\dots[/$]
Index: 26
Kind: Not

Definition: The equivalence class containing all infinite path fragments induced by execution fragments in \(TS(TA)\) of the form
\(s_0\xrightarrow{d_0^1}\dots\xrightarrow{d_0^{k_0}}s_0+d_0\xrightarrow{\alpha_0}s_1 \dots s_{n-1}\rightarrow\dots\rightarrow\xrightarrow{\alpha_{n-1} } s_n\xrightarrow{1} s_{n+1}\xrightarrow{1} s_n+2 \xrightarrow{1}\dots \) with \(\sum_{j=1}^{k_0} s_{i}^{j}=d_0\)
Page: 697
Section: 1.2
Variables: \(TA\) a TA,
\((d_i)_{i\le n}\)
Notation: [$]s_0\xRightarrow{d_0}s_1\dots\xRightarrow{d_{n-1} }s_n\xRightarrow{1} s_{n+1}\xRightarrow{1} s_{n+2}\xRightarrow{1}\dots[/$]
Index: 26
Kind: Not

Name: Timed CTL
Definition: State formula
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks
Index: 27
Kind: Def
Definition2: Path formula
Conjdef: Both
Abbreviation: TCTL

Name: Timed CTL state formula
Definition: Containing true
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks
Index: 27
Kind: Def
Definition2: containing atomic propositions,
Conjdef: The least set,
Definition3: containing atomic clock constraint,
Abbreviation: TCTL state formula
Definition4: closed under conjonction,
Definition5: closed under negation,
Definition6: closed under quantification of a variable over a path formula

Name: Timed CTL path formula
Definition: \(\Phi_1\mathcal{U}^J\Phi_2\) where \(J\) is an interval whose bounds are natural numbers and \(\Phi_i\)'s are state formula
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks
Index: 27
Kind: Def
Abbreviation: TCTL path formula

Definition: \(\text{true}\mathcal U^J\Phi\)
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks,
\(L\) an interval of real with natural or infinity bounds
\(\Phi\) a state formula
Notation: \(\lozenge^J\Phi\)
Index: 27
Kind: Def

Definition: \(\neg\exists \lozenge^J\neg\Phi\)
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks,
\(L\) an interval of real with natural or infinity bounds
\(\Phi\) a state formula
Notation: \(\forall\square^J\Phi\)
Index: 27
Kind: Def

Definition: \(\neg\forall \lozenge^J\neg\Phi\)
Page: 698
Section: 2
Variables: \(AP\) a set of atomic propositions
\(C\) a set of clocks,
\(L\) an interval of real with natural or infinity bounds
\(\Phi\) a state formula
Notation: \(\exists\square^J\Phi\)
Index: 27
Kind: Def

Question: In LCTL, absence of subscript on an operator indicates:
Answer: the interval is \(\mathbb R_{\ge0}\)
Page: 698
Chapter: 9
Section: 2
Index: 27
Kind: Def

Definition: True, negation and conjonction as usual
-\(s\models a\), for \(a\in AP\) iff \(a\in L(\ell)\)
-\(s\models g\), for \(g\in ACC(C)\) iff \(\eta\models g\)
-\(\forall \phi\) iff \(\pi\models\phi\) for each \(\Pi\in Paths_{div}(s)\)
-\(\exists \phi\) iff \(\pi\models\phi\) for some \(\Pi\in Paths_{div}(s)\)
Page: 701
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(a\in AP\),
\(g\in ACC(C)\),
\(J\subseteq\mathbb R_{\ge0}\),
\(s=\langle \ell,\eta\rangle\) a state in \(TS(TA)\)
\(\Phi\) a TCTL state fourmae
Notation: \(s\models\Phi\)
Index: 30
Kind: Def
Extra: Note the restriction of path divergence

Definition: there exists \(i\ge 0\), such that \(s_i+d\models\Psi\) for some \(d\in[0,d_i]\) with \[\sum_{k=0}^{i-1}d_k+d\in J\] and for all \(j\le i\), \(s_j+d'\models\Phi\lor\Psi\) for any \(d'\in[0,d_j]\) with \[\sum_{k=0}^{j-1}d_k+d'\le \sum_{k=0}^{i-1}d_k+d\].
Page: 701
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(a\in AP\),
\(g\in ACC(C)\),
\(J\subseteq\mathbb R_{\ge0}\),
[$]\pi=s_0\xRightarrow{d_0}s_1\dots\xRightarrow{d_{n-1} }s_n\xRightarrow{1} s_{n+1}\xRightarrow{1} s_{n+2}\xRightarrow{1}\dots[/$]
\(\Phi,\Psi\) TCTL states formulae
Notation: \(\pi\models\Phi\mathcal U^J\Psi\)
Index: 30
Kind: Def
Extra: Note the disjonction in the last case, different from CTL

Smaller0: \(\Phi\mathcal U\Psi\)
Greater0: \((\Phi\lor\Psi)\mathcal U\Psi\)
Page: 702
Chapter: 9
Section: 2
Variables: \(\Phi,\Psi\) CTL state formulae
Smaller to greater: is equivalent to
Hide sides: yes

Name: The satisfaction set of \(\Phi\)
Definition: The set of \(s\in Loc\times Eval(C)\) which models \(\phi\)
Page: 703
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(\Phi\) a TCTL state formulae
Index: 32
Kind: Def
Abbreviation: \(Sat(\Phi)\)

Name: \(TA\) satisfies \(\Phi\)
Definition: for each \(\ell_0\in Loc_0\), \(\langle \ell_0,0\rangle\models\Phi\)
Page: 703
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(\Phi\) a TCTL state formulae
Notation: \(TA\models\Phi\)
Index: 30
Kind: Def

Smaller0: \(TS(TA)\models_{TCTL}\Phi\)
Greater0: \(TS(TA)\models_{CTL}\Phi\)
Page: 704
Chapter: 9
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(\Phi\) a CTL state formulae
Index: 34
Kind: Ex
Counterexample: Let \(TA\) a TA with initial state \(q_0\) with invariant \([0,1]\), and a transition to \(q_1\), with property P.
Let \(\Phi=\forall\lozenge P\).
The time-divergent pathes of \(TA\) satisfies \(\Phi\), hence \(TS(TA)\models_{TCTL}\Phi\). However, the time convergent path which never crosses 1 does not satisfies \(\Phi\).
Hide sides: yes

Smaller0: \(s\models_{LCTL}\exists\square \text{true}\) for each \(s\in Reach(TS(TA))\)
Greater0: \(TA\) is timelock-free
Page: 704
Chapter: 9
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
Index: 35
Kind: Lem
Smaller to greater: iff

Smaller0: \(s\models_{LCTL}\exists\square \text{true}\)
Greater0: \(s\) is timelock-free
Page: 704
Chapter: 9
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(s\in Loc\)
Index: 35
Kind: Lem
Smaller to greater: iff

Smaller0: \(TA\models\forall\square\Phi\)
Greater0: \(\Phi\) holds in each accessible state in \(TS(TA)\)
Page: 704
Chapter: 9
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(\Phi\) a LCTL formulae
Index: 34
Kind: Ex
Smaller to greater: iff
Assuming: \(TA\) is timelock free

Smaller0: \(\Phi\) holds in each accessible state in \(TS(TA)\)
Greater0: \(TA\models\forall\square\Phi\)
Page: 704
Chapter: 9
Section: 2
Variables: \(TA=(Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)\) a TA,
\(\Phi\) a LCTL formulae
Index: 34
Kind: Ex
Counterexample: Takes \(\Phi=P\),
\(TA\) without diverging path