Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 10 - Probabilistic Systems=proba
Tags: ExampleOfBuriedTags hasSeenConjDef omitted
On every note of this deck, unless a note says otherwise:
Chapter: 10

Question: Difference between verifying probabilistic system and probabilistic verification ?
Answer: The first probability is inherent to the system. The second one is a qualification regarding technique used on the system
Page: 745
Chapter: 10

Name: A qualitative property
Definition: A property that happens almost surely/never occurs
Page: 746
Example: Reachability
Example2: persistence
Example3: repeated reachability

Name: Persistence property of \(e\)
Definition: «Eventually, \(e\) always hold»
Page: 746
Variables: \(e\) an event

Name: Repeated reachability property of \(e\)
Definition: \(e\) can be repeatedly reached
Page: 746
Variables: \(e\) an event

Name: A Markov chain
Definition: A tuple \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) with:
-\(S\) a set of states
-\(\mathbf P\) a transition probability function
-\(\iota_{init}\) the initial distribution
-\(AP\) is a set of atomic propositions, and
-\(L:S\to 2^{AP}\)
Page: 747
Section: 1
Kind: Def
Name2: A Discrete time Markov chain
Abbreviation: MC
Denoted by: \(\mathcal C\)

Name: A set of states of a markov chain
Page: 748
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC
Kind: Def
Denoted by: \(S\)
Cardinal: Countable nonempty

Name: A transition probability function
Definition: An element \(f:S\times S\to[0,1]\) such that \(\sum_{s'\in S}f(s,s')=1\)
Page: 748
Section: 1
Variables: \(S\) a set of states of a Markov Chain
Kind: Def
Denoted by: \(\mathbf P\)

Name: An initial distribution
Definition: \(f:S\to[0,1]\) such that \(\sum_{s\in S}f(s)=1\),
Page: 748
Section: 1
Variables: \(S\) a set of states of a Markov Chain
Kind: Def
Denoted by: \(\iota_{init}\)

Name: A finite MC
Definition: A MC whose set of states and of atomic propositions are finite
Page: 748
Section: 1
Kind: Def

Definition: \(\sum_{t\in T}\mathbf P(s,t)\)
Page: 748
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s\in S\),
\(T\subseteq S\)
Notation: \(\mathbf P(s,T)\)
Kind: Def

Name: The underlying digraph of \(\mathcal M\)
Definition: \((S,\{(s,s')\mid \mathbf P(s,s'){\gt}0\})\)
Page: 748
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC
Kind: Def

Name: A path in \(\mathcal M\)
Definition: A maximal path in its underlying digraph
Page: 748
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
Kind: Def

Definition: The set of states occurring infinitely often in \(\pi\)
Page: 749
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(\pi\) a path in \(\mathcal M\)
Notation: \(\text{inf}(\pi)\)
Kind: Def
Cardinal: Non-empty

Name: An absorbing state
Definition: A state which is its only successor
Page: 753
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
Index: 6
Kind: Def

Definition: Set of states \(S\)
Page: 753
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
Notation: \(TS(\mathcal M)\)
Definition2: Set of actions \(\{\tau\}\)
Conjdef: The TS
Definition3: \(s\xrightarrow{\tau}t\) if \(P(s,t)>0\)
Definition4: \(I\) the set of \(s\in S\) such that \(\iota_{\text{init}}(s)>0\),
Definition5: same labels: \(AP\) and \(L\)

Question: Omitted
Answer: Def of probability state
Page: 753
Chapter: 10
Section: 1

Name: The cylinder set of \(\hat\pi\)
Definition: The set of \(\pi\in Paths(\mathcal M)\) with prefix \(\hat\pi\)
Page: 757
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(\hat\pi=s_0\dots s_n\in Paths_{fin}(\mathcal M)\)
Abbreviation: \(Cyl(\hat\pi)\)

Name: The \(\sigma\)-algebra associated with \(\mathcal M\)
Definition: The smallest \(\sigma\)-algebra that contains all cylinder sets \(Cyl(\hat\pi)\) with \(\hat\pi\in Paths_{fin}(\mathcal M)\)
Page: 758
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
Notation: \(\mathfrak E^{\mathcal C}\)
Kind: Def

Definition: \(\Pi_{0\le i<n}\mathbf{P}(s_i,s_{i+1})\)
Page: 758
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s_0\dots s_n\) a path in \(\mathcal M\)
Notation: \(\mathbf{P}(s_0\dots s_n)\)
Kind: Def

Definition: \(\iota_{\text{init}}(s_0)\Pi_{0\le i<n}\mathbf{P}(s_i,s_{i+1})\)
Page: 758
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s_0\dots s_n\) a path in \(\mathcal M\)
Notation: \(PR^{\mathcal{M}}(s_0\dots s_n)\)
Kind: Def
Notation2: \(PR(s_0\dots s_n)\)

Definition: The function on \(S\) sending \(s\) on 1 and everything else to 0
Page: 758
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s\in S\)
Notation: \(\iota_s^1(t)\)
Kind: Def

Name: The probability for \(\phi\) to hold in state \(s\)
Definition: \(Pr^{\mathcal M}(\phi\in Paths(s)\mid\pi\models \phi)\)
Page: 759
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s\in S\)
\(\phi\) a LTL formula over \(AP\)
Notation: \(Pr^{\mathcal M}(s\models\phi)\)
Index: 12
Kind: Not

Name: The craps gambling game
Definition: Let come-out be the output of two dices.
If come-out is 7 or 11, win
If come-out is 2, 3 or 12, lose.
Otherwise, reroll until come-out or 7 is found. On 7, lost, on come-out win.
Page: 750
Section: 1
Index: 4
Kind: Ex

Question: The equation of \((x_s)_{s\in S}\):
Answer: \[\sum_{t\in S\setminus B}\mathbf{P}(s,t)\cdot x_t+\sum_{u\in B}\mathbf{P}(s,u)\], i.e. \[\vec x=\mathbf P\vec x+(P(s,B))_{s\in S}\]
Page: 760
Chapter: 10
Section: 1
Variables: \(\mathcal M=(S,\mathbf P,\iota_{init},AP,L)\) a MC,
\(s\in S\)
\(B\subseteq S\)
\(x_s\) the probability to reach \(B\) from \(s\)