[MUSIC] It is good to see you back for the second lecture of the module on probabilistic computation tree logic. We will take a look at the general model checking routine and we will also consider how to model check the next operator. First things first, how to do the general model-checking routine for pCTL? Question we want to answer is, does a state in a label DTMC satisfy a pCTL formula phi? What we have to do is, we have to recursively compute the set of states that satisfy phi. This is a concept that you know from CTL, the so-called satisfaction set. Once we have the satisfaction set, we can simply check whether a state s belongs to that satisfaction set or not. The good news is that for the non-probabilistic part of pCTL, this works exactly as for CTL. So the question we have to answer is. How to compute a satisfaction set for formulas that involve the probabilistic operator? I already told you we have to do a recursive computation and this recursive computation follows the character of the formula. So we have to build a parse tree of the formula, and let's do that for an example. Here I've done it for you. The formula is quite complicated and it also involves operators that we haven't seen so far. But they can simply be built from the ingredients that you have seen in the syntax. So this translates to say red follows green. Translates to not red or green. And also the end was not in the syntax. But you know that end can be built from the negation and the or operator. So the only thing that is new now is the probability operator. And you have to be careful, because in the nodes of the parse trees, you always have to have state formulas. That is something important to remember. So you have both the probability operator and the until operator in this node. And then you have the left part of the until operator goes in this part of the tree, and the right part goes into that part of the tree. Now you start with model checking the leaves of this parse tree, compute the satisfaction set, go one level up, compute the next satisfaction set and so on until you have obtained the satisfaction set for the whole formula. So for the non-probabilistic part of PCTL, this works exactly as for CTL. Imagine that you want the satisfaction set of an atomic property. You just have to accumulate all states from the state space that are assigned this atomic property as a label. If you have to negate a formula phi, and we assume that you have the satisfaction set of that formula phi. The negation is obtained by taking the states base without those states that are in the satisfaction set of phi. Now if you want the conjunction of two PCTL formulas phi 1 and phi 2, you just take the combination of both satisfaction sets. Now the question that remains is how to model check the probabilistic part of PCTL, and that is all formulas that involve the probability operator. So we need to compute the probabilities for all paths that start in a certain state s. As promised, I'll start with the easier one of the two path operators, namely the next operator. And what we want to know is whether a state s in the satisfaction set of formula that involves next phi. And this is the case if the probability for all paths starting in s matching, fulfilling this path property, small phi actually matches the probability bound p. How do we do that? We still do a recursive computation. We assume that we have the satisfactions of ro phi and then we can use this formula to check whether the state s is in that satisfaction set. So for each state s we need to accumulate the probability to move from state s to any of the state s prime that is in the satisfaction set of phi. Now how do we do that? Let's take a look at a not so small example. We have six states. And we want to check whether the probability to be in a state that fulfills b in the next step is greater or equal to 0.8. So where are the b states? That are those that are highlighted in green. And now I have already written down the probability matrix for you. And now what we need to do is for each state, accumulate the probability to be in a b state in next step so let's do that. So for state 0, we have to accumulate 0 and 0. It's easy, 0. First state 1, we can reach state 0 or state 3 in one step, both are not in the satisfaction set of p. So also for this one we have a 0. State 3 is absorbing, so it will, I'm sorry, let's do stage 2 first. State 2 can move to 4, and 5, and 3, but only 4 and 5 are in the satisfaction set of b, so we have to accumulate these two probabilities. And that is the 0.8. Now, we do stage 3, we stay in state 3. State 3 is not a b state so the probability is 0. State 4 is a b state and in the next step, we can only stay there so probability is 1. And state 5, you can stay in state 5 or you can go back to state b. But both are b states so also here the probability is 1. So let me clean the solution up for you. And we obtain this vector that's the one that I just derived. And from that vector, you can now derive the satisfaction set by comparing the computed probabilities with the probability bound in the next formula. And the probability bound there is greater than or equal to 0.8, so only states 2, 4 and 5 are in the satisfaction set. So now you already know how to model check formulas that only involve the next operator. [MUSIC]