\input{header.tex}
\title{Probabilistic Model Checking (Sheet \#1)}
\author{Marius Gavrilescu}
\date{}
\maketitle
\newcommand{\PP}{\operatorname{P}}
\newcommand{\X}{\operatorname{X}}
\newcommand{\F}{\operatorname{F}}
\newcommand{\G}{\operatorname{G}}
\newcommand{\A}{\operatorname{A}}
\newcommand{\E}{\operatorname{E}}
\begin{enumerate}
\item % 1.
\begin{enumerate}
\item $\frac{1}{3}+\frac{2}{3}(\frac{1}{4}+\frac{1}{4})=\frac{2}{3}$
\item % (b)
$s_3$ can only be reached from $s_0,s_5,s_4,s_3$. The
probability is $1$ from $s_3$ and $s_4$,
$\frac{1}{2}\frac{1}{4}=\frac{1}{8}$ from $s_0$, and
$\frac{1}{4}+\frac{1}{2}\frac{2}{3}\frac{1}{4}=\frac{1}{3}$ from
$s_5$ (because we can go $s_5s_4s_3$, or $s_5s_0s_5s_4s_3$ and both
options take no more than 4 transitions).
\item % (c)
Same as before, but $s_0$ and $s_5$ get more complicated.
$s_0$ has probability
$(\frac{2}{3}\frac{1}{4})(1+\frac{1}{3}+\frac{1}{9}+\ldots)$. The
first term represents the probability of going $s_0s_5s_4s_3$, and
the second term represents the probability of doing $s_0s_5s_0$ 0
times, 1 time, 2 times, and so on. The total probabiliy is
$\frac{1}{6}\frac{3}{2}$ which is $\frac{1}{4}$.
Now we can use this to compute $s_5$'s probability, which is
$\frac{1}{4}+\frac{1}{2}\frac{1}{4}$ (because we go right with
probability $\frac{1}{4}$, and we go to $s_0$ with probability
$\frac{1}{2}$), so this is $\frac{3}{8}$.
\item % (d)
To not reach the states $A\cup B$ means to get stuck in state $s_1$
or $s_6$ or in the $s_0s_5$ loop. All of these paths have
probability 0, so the probability of reaching a state in $A\cup B$
is 1.
\item % (e)
With the same logic as above, the probability of getting stuck in
one of those loops is 0, so the probability of visiting $A\cup B$
infinitely often is also 1.
\end{enumerate}
\item % 2.
\begin{enumerate}
\item % (a)
We can represent this set as the complement of the set of all paths
that contain a state not in A. This set is the union of all cylinder
sets $\operatorname{Cyl}(\omega)$ where $\omega$ contains only
states in $A$, except for the last state. There are a countable
number of such cylinder sets, so their union is measurable, and its
complement is also measurable.
\item % (b)
We can represent this set as the intersection of the set from part
(a) and the set of paths whose fifth state is in $B$. This latter
set is the union of cylinder sets $\operatorname{Cyl}(\omega)$ where
$\omega$ has length 5 (or 6, depending on how we interpret the
problem statement) and its last state is in $B$. There is a finite
number of such cylinder sets, so their union is measurable. The
intersection is measurable too, and that is the set we are looking
for.
\end{enumerate}
\item % 3.
The states are $a_i$ with $0\le i\le n$, representing that player 1
has $i$ coins and player 2 has $n-i$ coins. Starting state is $a_m$.
We have transitions with probability $0.5$ from $a_i$ to $a_{i-1}$
and to $a_{i+1}$ for all $0* 0.5}[\F \text{win1}]$.
The last statement can be expressed as
$\PP_{\le 0.1} [\F^{\le 5}\PP_{> 0}[\X \text{win}1]]$.
\clearpage
\item % 4.
$\E\G a$ means there exists a path starting from here such that all
its states satisfy $a$. $\PP_{> 0}[\G a]$ means that it is possible
to find a path starting from here such that all its states satisfy
$a$. These two statements are equivalent.
We know that
$s\vDash \PP_{\ge 1}[\G a] \iff s\vDash \PP_{\le 0}[\F \neg a]\iff s\not\vDash \PP_{> 0}[\F \neg a]\iff s\not\vDash \E\F\neg a\iff s\vDash AG a$.
So the first pair of statements are also equivalent.
\item % 5.
$\displaystyle P=\begin{bmatrix}
0 & 0.5 & 0 & 0.5 & 0 & 0\\
0 & 0 & 1 & 0 & 0 & 0\\
0 & 1 & 0 & 0 & 0 & 0\\
0 & 0 & 0 & 0 & 1 & 0\\
0 & 0 & 0 & 0 & p & 1-p\\
0 & 0 & 0 & 1 & 0 & 0
\end{bmatrix}$
$\pi(0)=\begin{bmatrix}1 & 0 & 0 & 0 & 0 & 0\end{bmatrix}$
We can compute the long-run probability of being in $s_2$ to be $0.25$.
For state $s_4$, the probability of reaching its BSCC is
$\frac{1}{2}$. So the probability of being in $\{s_2, s_4\}$ is
$0.25+0.5*p$ where $p$ is the probability of being in $s_4$ given
that we are in its BSCC. We need to solve:
$x\cdot P=x$ with $x$ starting as
$\begin{bmatrix}0 & 0 & 0 & 1 & 0 & 0\end{bmatrix}$.
\end{enumerate}
\end{document}
*