\input{header.tex}
\title{Probabilistic Model Checking (Sheet \#3)}
\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}}
\newcommand{\U}{\operatorname{U}}
\newcommand{\Sat}{\operatorname{Sat}}
\newcommand{\Prob}{\operatorname{Prob}}
\begin{enumerate}
\item % 1.
We assume we can never reach state 22, because when a process
reaches state 2 it moves back to state 0 before the other process
can change state.
The first statement can be represented by the PCTL formula
$\neg \text{ one}\lor\PP_{\ge 1}[\F \text{ zero}]$ where
$\text{one} = \{01, 10, 11\}$ and $\text{zero} = \{00\}$.
This formula is false, as we can manufacture an adversary which from
state 10 always goes to 11 and from state 01 always goes to 11. Now
from state 11 we will go to either 12 or 21, then to either 10 or
01, and then back to 11. So we will never reach 00.
The second statement is $\PP_{\ge 1}[\G\F \text{ A2}]$ where
$\text{A2} = \{20, 21\}$. It is false, because we can create an
adversary which always goes from 00 to 01 and always goes from 01 to
02. Now starting from 00 we always go to 01, then always to 02, then
always to 00. So we never reach 20 nor 21.
The third statement is $\PP_{\ge 1}[\G\F \text{ some2}]$ where
$\text{some2}=\{20, 21, 02, 12\}$. This statement is true, because
there exists no loop that avoids states 02, 20, 21, 12. We can go
from 00 to 01 or 10, but then we are forced to go to 11, and from 11
we can only go to 21 or 12.
\setcounter{enumi}{2}
\item % 3.
The first formula is not satisfiable. If $s\vDash\PP_{>0.5}[\X a]$
then for any adversary the probability of $\X a$ is greater than
0.5. As $\X a$ implies $\F a$, for any adversary the probability of
$\F a$ is greater than 0.5. Therefore $s\not\vDash\PP_{<0.5}[\F a]$.
The second formula is satisfiable. In the given MDP, there is an
action (going left) from $s_0$ that gives probability 0 of $\F a$,
so $s_0\not\vDash\PP_{\ge 0.4}[\F a]$, and an action (goin right)
that gives probability 1 of $\X a$, so
$s_0\not\vDash\PP_{\le 0.6}[\X a]$. Therefore
$s_0\vDash\neg\PP_{\le 0.6}[\X a]\land\neg\PP_{\ge 0.4}[\F a]$.
\clearpage
\setcounter{enumi}{1}
\item % 2.
For $b\lor \PP_{<0.4}[\X a]$, we note that all states that do not
have a transition to $s_5$ have probability 0 of $\X a$, and
therefore must satisfy the property. These states are
$s_0, s_3, s_4, s_5$.
We are left with $s_1$ and $s_2$. For $s_1$ there is a single
possible action, which leads to $s_5$ with probability 0.5. So
$s_1\not\vDash\PP_{<0.4}[\X a]$.
For $s_2$, there is an adversary that chooses the bottom action,
which leads to $s_5$ with probability 0.5. So
$s_2\not\vDash\PP_{<0.4}[\X a]$.
Therefore only $s_0, s_3, s_4, s_5\vDash b\lor\PP_{<0.4}[\X a]$.
For $\PP_{\le 0.3}[\neg a\U b]$, we want maximum probabilities.
Prob0A gives us\\
$S^{\text{no}}=S\setminus\{s_0, s_3, s_4, s_2, s_1\}=\{s_5\}$.
Now we compute $S^{\text{yes}}$ via Prob1E. We start with $R=S$,
then $R=\{s_0, s_1, s_2, s_3, s_4\}$, then $R=\{s_0, s_3\}$. So
$S^{\text{yes}}=\{s_0, s_3\}$. The only states left are
$s_1, s_2, s_4$.
There are two possible adversaries for $s_4$, and the one that
chooses the transition to $s_3$ will satisfy the formula
$\neg a\U b$ with probability 1. So the maximum probability for
$s_4$ is more than 0.3.
There are two possible memoryless adversaries for $s_2$. The one
that takes the bottom action has a 0.5 probability of going to $s_5$
(which satisfies $\neg a\U b$ with maximum probability 0) and a 0.5
probability of going to $s_4$ (which satisfies $\neg a\U b$ with
maximum probability 1). Therefore the maximum probability of
satisfying $\neg a\U b$ is 0.5, which is more than 0.3.
$s_1$ has a single action, with probability 0.5 of going to $s_5$
(which does not satisfy $\neg a\U b$) and probability 0.5 of going
to $s_2$. So the maximum probability for $s_1$ is 0.25, which is
less than 0.3.
Therefore only $s_1, s_5\vDash\PP_{\le 0.3}[\neg a\U b]$.
For $\PP_{>0}[\neg a\U b]$ we need minimum probabilities.
Prob0E gives us
$S^{\text{no}}=S\setminus\{s_0, s_3\}=\{s_1, s_2, s_4, s_5\}$
because $s_4$ has a transition to $s_1$ which makes $s_0$
unreachable without going through $s_5$ first.
Now we are left with two states that could have nonzero
probabilities. Both of these have a single action. $s_0$ already
satisfies the property because it is in $Sat(b)$, and then $s_3$
also satisfies the property because it satisfies $\neg a$ and it is
guaranteed to be immediately followed by $s_0$.
So only $s_0, s_3\vDash \PP_{>0}[\neg a\U b]$.
A memoryless adversary for the second property would choose he
bottom action for $s_2$, left action for $s_4$, bottom action for
$s_5$.
Counterexample for $s_2$ is the path $s_2s_4s_3s_0$ which has
probability 0.5 and satisfies $\neg a\U b$.
End components are $\{s_1, s_2, s_5\}, \{s_1, s_2, s_4, s_5\}$,
$\{s_0, s_1, s_2, s_3, s_4, s_5\}$.
We are guaranteed to reach an end component and all end components
include $s_5$, so $s_5$ will always be visited infinitely often. So
every state satisfies $\PP_{\ge 1}[\G\F a]$.
There is an adversary that keeps us in the $\{s_1, s_2, s_5\}$ end
component forever, in which case the probability of $\G\F b$ is 0.
There is also an adversary that keeps us in the
$\{s_0, s_1, s_2, s_3, s_4, s_5\}$ end component forever, in which
case $s_0$ is visited infinitely often and so the probability of
$\G\F b$ is 1.
So the minimum probability of this property being satisfied (from
any state) is 0, and the maximum probability is 1. Therefore none of
the last three formulae are satisfied by any sate.
\end{enumerate}
\end{document}