Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 07 - Equivalence

Definition: TCTL restricted to intervals being \([0,\infty)\)
Page: 706
Chapter: 9
Section: 3.1
Notation: \(\text{TCTL}_\lozenge\)

Definition: The function sending \(z\) to \(d\), and equal to \(\eta\) otherwise
Page: 707
Chapter: 9
Section: 3.1
Variables: \(C\) a set of clock,
\(z\not\in C\),
\(\eta\) a valuation of \(C\)
Notation: \(\eta\{z:=d\}\)
Index: 36
Kind: Not

Definition: \(\langle\ell,\eta\{z:=d\}\rangle \)
Page: 707
Chapter: 9
Section: 3.1
Variables: \(C\) a set of clock,
\(z\not\in C\)
\(TA\) a timed automaton over \(C\)
\(s=\langle\ell,\eta\rangle\) a state
Notation: \(s\{z:=d\}\)
Index: 36
Kind: Not

Definition: \(TA\) with set set of clocks \(C\cup \{z\}\)
Page: 707
Chapter: 9
Section: 3.1
Variables: \(C\) a set of clock,
\(z\not\in C\)
\(TA\) a timed automaton over \(C\)
Notation: \(TA\oplus z\)
Index: 37
Kind: Not

Smaller0: \(s\models_{TCTL}Q(\Phi\mathcal U^J\Psi)\)
Greater0: \(s\{z:=0\}\models_{TCTL}Q((\Phi\lor\Psi)\mathcal U(z\in J)\land\Psi)\) for \(z\not\in C\)
Page: 707
Chapter: 9
Section: 3.1
Variables: \(C\) a set of clock,
\(TA\) a timed automaton over \(C\),
\(s\) a location of \(TA\),
\(Q\) a quantifier,
\(J\) an interval,
\(\Phi,\Psi\) TCTL state formulae
Index: 37
Kind: Theo
Smaller to greater: iff