[MUSIC] Welcome back to the course on Quantitative Model Checking. In this third module, we'll deal with Probabilistic Computation Tree Logic, which is abbreviated as PCTL. And in this first lecture, we'll take a look at the syntax of PCTL. Now, before we can do that, we need to reconsider discrete-time Markov chains, and we need to enhance them by the so-called labelling function. Now, what is a labelling function? It assigns labels to states. It can be very simple things, like red or green, if you think about the traffic light. And formally, it is a function that assigns zero or more labels to elements of the states brace. Now we want to express properties over these labeled DTMCs. And of course you still know how to compute steady-state and transient-state probabilities for DTMCs. And now, we want to associate these with the atomic properties or labels as we call them. Can we express path-based properties? Something like this. Is the probability to run along green states, with finally reaching a red state, smaller than 1%? Now how do we formalize pCTL properties. As in CTL, we have to distinguish between state-formulas and path-formulas. Now, the good news is that the first part of the state-formulas looks exactly like what you've seen in CTL. The only thing we have to add is the so called probability operator. And that is what you see here. What does the probability operator tell us? Well, it compares the probability that all the paths that start in a certain state fulfill this path property, which is wrapped inside the probability operator, that they fulfill this comparison. So, what we have is the comparison operator, which can be small or equal, greater equal, and we have this probability, p. And then this probability operator checks whether the probability to take such a path matches its probability bound. Now, this concept is similar to quantification in CTL. You have seen the existing and the all quanta and they can be translated to pCTL using the probability operator and we compare with greater than 0 for the existence and with greater equal to 1 for the all quanta. Now, let's move to path-formulas. Path-formulas can be two things in pCTL. They can either be next or until. And this is what we call next, and this is until. Next reasons about the state that you reach in the next step, and until reasons about the whole path and it comes with a sub-superscript, smaller or equal to k, and that is the number of steps that you have to reach such a state. So phi until psi means phi holds along the path, until you reach a state where psi holds and you have to reach that in at most k steps. So this is the formal syntax of pCTL and this is what we'll use to express properties over LDTMCs. Now I have talked about states and paths that fulfil certain properties clearly. A path can only fulfil a path property and a state can only fulfil a state property. Now, this is what a path looks like. It's just states after each other and they can satisfy the next or the ante formula. And then we translate this to the level of states and we say state s fulfills this probability operator with the path operator, sorry with the path-formula wrapped inside. Again, if the probability of all the paths starting from s, fulfill this comparison. This is an example. We have the state s, this is where we start, and then here you see all the paths that start in s. And we distinguish between those that fulfill the path property, and that is green ones here below, and those that do not fulfill this path property, and that is the blue ones on top. And then we accumulate the probability for those paths who fulfill the property and we compare that with the probability bound. Now, let me give you some examples of pCTL requirements. For example, if we want to express the probability of not going down in the next step is at least 95%. I would write this using the next operator. So next down, and then I need the probability operator, and is at least zero point nine five. So let's take another one, the probability of going down within five steps is at most one percent, well five steps I need the until operator. And it gets this superscript, smaller equal to five. I want to reach a down state. And now I see that there's mistake in the first formula. I'm sorry. Should, of course, be not down. Be careful. Now, coming back to the second one, we want to reach a down state this time. We don't say anything about the states that we visit on the path to down, so I can just put true true here. And then I need to wrap the probability operator around. And this is, at most, 1%, so that is smaller or equal to 0.01. And one more, the probability of going down within five steps after continuously operating with at least two processors is at most 1%. This also is an until formula, it's slightly more complicated. Until, smaller equal to five, going down again, but now I have a requirement for the states that I visit until I reached down, and this is up to or up three, imagine that you have a system with at most three processors that can go up and down. And then again, I need the probability operator and this is at most 1%. So let me clean this up for you. If you're careful, you see now that this looks slightly different than what I have written for you and this is just reachability which you know from CTL. So true until down is equivalent to eventually down. So, If you want to know how to actually check such properties, I recommend you keep watching this lecture series. [MUSIC]
