2024-10-28 PSV
DTMC
1.
1. Give the formal semantic of PCTL, interpreted over DTMC.
$$M\vDash \varphi:= s_0 \vDash \varphi$$
Let $M=(S_0,\dots)$
$$s\vDash \neg \varphi := \neg(s\vDash \varphi)$$
$$s\vDash p := p\in V(s)$$
$$s\vDash \varphi_1 \land \varphi_2 = (s\vDash \varphi_1) \land (s \vDash \varphi_2)$$
$$s\vDash P_{\tilde q}[\psi] = P(s\vDash \psi)~q$$
$$s\vDash P_{\tilde q}[\psi] = P\{w\in \text{Paths}(s)\mid w \vDash \psi\}\tilde q$$
$$\omega \vDash X\varphi := \omega_1 \vDash \varphi$$
$$\omega \vDash \varphi_1 U \varphi_2 := \exists y w_y\vDash \varphi_2 \land \forall zB has probability 0.5,
A to itself has probability 0.5 and B to itself has probability 1.
We see that AF B is false because A looping on itself is a feasible path, put
the probability of this occoring is zero, hence the chance that there will
be a B is 1, hence $P_{\geq 1}[B]=1$ is true.
3.
- We write $x_i$ as the the probability is true from node $i$. We see that
$$x_5=0,x_4=0,x_2=1,x_3=1,x_1=0.5x_2 + 0.5x_0, x_0=0.9x_1$$
So $$x_0=0.9x_1=0.9(0.5x_2+0.5x_0) = 0.45x_2+0.45x_0 = 0.45+0.45x_0$$
so $$0.55x_0 = 0.45$$
so $$11x_0 = 9$$
so $$x_0 = 9/11$$
this probability is less than 0.81, hence it is not treu
- We saw that x_0<0.82, hence this is true
- ?
4.
- We write $x_i$ as the the probability is true from node $i$. We see that
$$x_5 = 1,x_4=1,x_2=0,x_3=0.5x_0,x_0=0.9x_1+0.1x_4$$
MDP
1. The probability of $\phi$ is at least $c$ and the probability of $\phi$ is at most $c$
**Note:** Memoryless adversary means that the same choice is made at every node.
**Note:** For DTMC we had that $S^\text{No} = \overline{R}$ where $R= \text{sat}(E(p U
q))$. Now $R= \text{sat}(E(p U q)\forall \text{ adversaries)$.