Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 07 - Equivalence=CTL*
Tags: fromImplication hasSeenConjDef toBinaryRelation typToBinary closed fromMath mathToSee

Name: \(M_1\) is refined by \(M_2\)
Page: 449
Chapter: 9
Variables: \(M_1,M_2\) two models
Name2: \(M_2\) is an abstraction of \(M_1\)
Name3: \(M_1\) is a correct implementation of \(M_2\)

Name: A bisimulation for \((TS_1,TS_2)\)
Definition: \(\forall s_i\in I_i(\exists s_{3-i}\in I_{3-i}. (s_1,s_2)\in R))\)
Page: 451
Chapter: 9
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) TSs
Index: 1
Kind: Def
Definition2: for all \((s_1,s_2)\in R\), \(L_1(s_1)=L_2(s_2)\),
Conjdef: A binary relation \(r\subseteq S_1\times S_2\) such that
Definition3: for all \((s_1,s_2)\in R\), if \(s'_i\in Post(s_i)\) there exists \(s_{3-i}\in Post(s_{3-i})\) with \((s'_1,s'_2)\in R\)
Denoted by: \(\mathcal R\)
Assuming: Both \(AP\) are equal

Page: 451, 453
Definition: Two TSs between which there exists a bisimulation
Chapter: 9
Notation: \(\sim\) on TSs
Name: Bisimulation-equivalent TS
Kind: Def, Lem
Index: 1, 4
Transitive: Equivalence relation
Name2: Bisimilar TS

Smaller0: \(TS_1\sim TS_2\)
Greater0: \(Traces(TS_1)=Traces(TS_2)\)
Page: 456
Chapter: 9
Section: 1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,APi,L_i)\) TSs,
Index: 6
Kind: Theo

Name: A bisimulation for \(TS\)
Definition: for each \((s_1,s_2)\in r\), \(L(s_1)=L(s_2)\),
Page: 456
Chapter: 9
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) TS,
Index: 7
Kind: Def
Definition2: \(s'_i\in Post(s_i)\) implies there exists \(s'_{3-i}\in Post(s_{3-i})\) with \((s'_1,s'_2)\in r\)
Conjdef: A binary relation \(r\) on \(S\) such that
Denoted by: \(\mathcal R\)

Page: 456
Definition: Two states \((s_1,s_2)\) such that there exists a bisimulation \(\mathcal R\) for \(TS\) with \((s_1,s_2)\in \mathcal R\)
Chapter: 9
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) TSs,
Notation: \(\sim_{TS}\)
Name: Bisimulation equivalent states of \(TS\)
Kind: Def
Index: 7
Transitive: Equivalence relation
Name2: Bisimilar states of \(TS\)

Smaller0: \(s_1\sim _{TS}s_2\)
Greater0: \(TS_{s_1}\sim TS_{s_2}\)
Page: 457
Chapter: 9
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) TS,
\(s_1,s_2\in S\)
Smaller to greater: iff

Definition: \(\biguplus S_i\)
Page: 457
Chapter: 9
Section: 1.1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP,L_i)\) TS,
Notation: \(\bigoplus TS_i\)
Definition2: \(\bigcup Act_i\)
Conjdef: The TS
Definition3: \(\bigcup \to_i\)
Extra: no name in the book
Definition4: \(\bigcup I_i\)
Definition5: \(AP\)
Definition6: \(L(s)\) being \(L_i(s)\) for \(s\in S_i\).

Definition: for each state \(C\) belonging to \((S_1\uplus S_2)/\sim_{TS_1\oplus TS_2}\), \(C\) intersects \(I_1\) iff it intersects \(I_2\)
Page: 457
Chapter: 9
Section: 1.1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP,L_i)\) TS,
Notation: \(TS_1\sim TS_2\)

Question: The coarsest bisimulation for \(TS\) is
Answer: \(\sim_{TS}\)
Page: 457
Chapter: 7
Section: 1.1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP,L_i)\) TS,
Index: 8
Kind: Lem

Name: The \(\mathcal R\)-equivalence class of \(r\)
Definition: The set of elements \(s'\) such that \((s,s')\in \mathcal R\)
Page: 457
Chapter: 9
Section: 1.1
Variables: \(S\) a set,
\(\mathcal R\) an equivalence relation on \(S\),
\(s\in S\)
Notation: \([s]_{\mathcal R}\)
Index: 10
Kind: Not

Smaller0: \([s]_{\mathcal R}=[s']_{\mathcal R}\)
Greater0: \(s'\in [s]_{\mathcal R}\)
Page: 458
Chapter: 9
Section: 1.1
Variables: \(S\) a set,
\(\mathcal R\) an equivalence relation on \(S\),
\(s,s'\in S\)
Index: 10
Kind: Not
Smaller to greater: iff

Name: The quotient space of \(S\) under \(\mathcal R\)
Definition: The set of \([s]_{\mathcal R}\) for \(s\in S\)
Page: 458
Chapter: 9
Section: 1.1
Variables: \(S\) a set,
\(\mathcal R\) an equivalence relation on \(S\)
Notation: \(S/\mathcal R\)
Index: 10
Kind: Not

Name: The bisimulation quotient of \(TS\)
Definition: Set of states: \(S/\sim\)
Page: 459
Chapter: 7
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\sim\) a bisimulation
Notation: \(TS/\sim\)
Index: 11
Kind: Def
Definition2: Actions: \(\{\tau\}\)
Conjdef: The transition system
Definition3: Transitions: \([s]_\sim\xrightarrow\tau'[s']_\sim\) for \(s\xrightarrow\alpha s'\)
Definition4: Initial states: \(\{[s]_\sim\mid s\in I\}\)
Definition5: Labels \(AP\) and labelling \(L'([s]_\sim)=L(s)\)

Smaller0: \(TS\)
Greater0: \(TS/\sim\)
Page: 459
Chapter: 7
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\sim\) a bisimulation
Index: 11
Kind: Def
Smaller to greater: \(\sim\)

Name: A bisimulation for \((TS_1,TS_2)\)
Definition: \(\forall s_i\in I_i(\exists s_{3-i}\in I_{3-i}. (s_1,s_2)\in R))\)
Page: 451
Chapter: 7
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,APi,L_i)\) TSs
Index: 1
Kind: Def
Definition2: for all \((s_1,s_2)\in R\):
\(L_1(s_1)=L_2(s_2)\),
Conjdef: A binary relation \(r\subseteq S_1\times S_2\) such that
Definition3: for all \((s_1,s_2)\in R\):
if \(s'_i\in Post(s_i)\) there exists \(s_{3-i}\in Post(s_{3-i})\) with \((s'_1,s'_2)\in R\)
Denoted by: \(\mathcal R\)
Assuming: Both \(AP\) are equal

Smaller0: \(TS_i\sim^{Act}TS'_i\)
Greater0: \(TS_i||_HTS_2\sim^{Act}TS'_1||_HTS'_2\)
Page: 466
Chapter: 9
Section: 1.2
Variables: \(TS_i, TS'_i\) TSs over the \(Act_i\)
\(H\subseteq Act_1\cap Act_2\)
Index: 16
Kind: Lem

Question: there exists a path \(\pi_2=(s_{2,i})\) such that
Answer: they have the same length and \((s_{1,i},s_{2,i})\in\mathcal R\)
Page: 454
Chapter: 9
Section: 1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,APi,L_i)\) TSs,
\(\mathcal R\) a bisimulation for \((TS_1,TS_2)\),
\((s_{1,0},s_{2,0})\in\mathcal R\),
\(\pi_1=(s_{1,i})\) a path in \(TS_1\)
Index: 5
Kind: Lem

Name: Congruence of action-based TS
Page: 466
Section: 1.2
Chapter: 9
Index: 16
Kind: Lem
Under: hand-shaking