[SOUND] So let's take a deeper look into the semantics of CTL. In order to do that we need the so called satisfaction relation and we need that both for state formulas and for path formulas. But I would like to start with state formulas, so. This symbol is used to express the satisfaction relation and this means a stay s satisfies the property to, well, this is always the case, so we do not need a further specification. Let's move to the next one state S satisfies an atomic property A if A is in the leveling set of that state S. Then, a state S is in the satisfaction relation of phi one and phi two If s satisfies phi 1 and s satisfies phi 2. And I use satisfy as a short-term notation for is in a satisfactory relation with. Then, s satisfies not phi if well s is not in the satisfaction relation with fie. That is very straight forward I would day. Now, we need to take a look at the path formulas, so exists fie and for all fie. So what is the semantics, s satisfies exists phi if there is a path which are called pi here starting in state s, such that this path satisfies the path phi. Now for all, this goes analogously. So for each path, pi now, that starts In state s, we require that this path satisfies the path property fine. Okay then we also need to define the so-called satisfaction set for a state formula phi and this is written at sat phi. And it is defined as the set of states in the state space that satisfy these state formula phi. So this is the so-called satisfaction set. Now, let's take a deeper look at the semantics of path formulas. We need to have this path, pi, which starts at S zero as one, as two, and so on, and this is an infinite path fragment. Now, we can have either next phi or phi 1 until phi 2. And such a path satisfies next phi, if well, s1, the next stage on that path satisfies the state formula capital phi here. Now, the until formula is holes for this path find. If there exists a j and j needs to be greater or equal to zero, such that for this state this corresponds to the index j the state formula phi 2 holds. And for all states before that, so that is for all states sk with k is in between 0 and smaller than j. We require that those sk they all fulfill the state formula fi 1 which comes before the antlr operator. yeah, so this is the semantics of the two path formulas that we can have and we derived the eventually and always a pleasure and of course we want to know what is the semantics of those operators. Well, a path pi satisfies eventually phi if well, and this is just a simplified version of the Rem that eventually phi is the same as true until phi. So we only require that there is such a j such that the stead Sj fulfills this state formula, capital fi. And then the always fi holds if for all j greater equal to 0, the corresponding states fulfill the state capital fi again. Yeah, so this is eventually an always. So, how to compute this satisfaction set for, for example, the next operator. You've seen the semantics, which is repeated here on top. Let's take a look at this example. We want to check whether there exists a path such that next phi. Let's imagine that this phi is the same as red and now we want to check this for the state S that is here, the green one. And you immediately see that there is such a successor which is read, and that is this one. Now the other two successors, they are not read, but that doesn't matter because we are checking for exists next read. What are we formally doing? Well, we have checking whether the intersection of, all the successors of s and they're in the set posts s and the Sat Satisfaction set for the state from unit phi. That is this one, is non-empty, so as soon as you have at least one successor that is in the satisfaction set of phi, the state s, fulfills this formula. How does this change if we check for all next phi. Well, here again we check for the green state and now in this computation tree all the successor states are red. So you can see immediately, that the green state fulfills this formula. And again, I would like to ask the question what are we checking formally? Well here we're checking whether the set of successors of s is a subset of the satisfaction set of phi. And if that is the case, s fulfills this for next phi, so now we have seen how to check the next operator but how is this done for other operators? Here comes a set of examples, exists eventually red, well, if we check that for this [INAUDIBLE] set, you can see that this formula holds, why? Because there are even two path that lead you eventually to a red and for this property, it would have been enough if we had one such path. Now, the next example is exists always red. So we are looking for at least one path that consists of only red states. Yes, and we have that, it's this one, so also here, the roots state fulfills this formula. The next one is a bit more complicated exists yellow until red. That's what you can read here. We are looking for at least one path again such that yellow holds until we hit a red side. And even though you cannot see the right part of the tree, it doesn't matter. You can see that here we have such a path. Yellow, yellow until red, so also here are the roots that fulfills that property. Now, three more examples. Now, I have used the for all operator instead of exists, so the first one, for all, eventually wraps. So, now we have to check whether from this root side, all paths eventually hit a red side. And, yes, you can immediately see this is the case, so here also this starting state fulfilled the formula. Next one, for always red and now, if you paid attention, you know, for always, say something about all the states in the states space. Yeah, why? Because you want to ensure that for all states, sorry, for all path originating in the initial state, you only hit red states. And if all states in the states are red, this is immediately valid. So also here, this computation tree and with that this starting state here fulfills the formula. Now, one more again and until formula, now we want to see whether for all yellow until red. So now, we have to check that for all the paths, that all the paths that originate here fulfill yellow until red. And you can, again, immediately see that here yellow, yellow, red and that one also yellow, yellow, red. Here, yellow, yellow red either way you go, you've fulfilled the formula. And also, the last one fulfills, sorry, you only have to go until here. Yellow, red and then, it is done. So that is an illustration of the semantics and now the question that remains is how do we automate the CTL model checking procedure? So what is given is a little transition system T and a CTL formula phi over a set of atomic properties. And also we need to S0 and that is the set of the starting states. And then the question is does this labelled transition system satisfy the CTL property, capital phi. And the idea for model checking now is to compute the satisfaction set for phi, which is defined as the set of states from the state space that fulfill phi. And then once we have this satisfaction set, we simply check whether the set of initial states Is a subset of this and satisfaction set. Well of course, you need to know how to compute this satisfaction set and this you will learn throughout the path of this course Something I can tell you is that the idea is to perform this computation recursively and we do the inner subformulas first. So basically you have to identify all of the subformulas sign of the state from your file you want to check and then compute the satisfaction set for each of these subformulas. Then we replace the subformulas by a new atomic proposition, a side which holds for each state that is in the satisfaction set of psi. And then you can check whether the set of initial states is a subset of the satisfaction set of phi, which you can compute based on the Satisfaction set for all the subformula. So it does a recursive procedure that we're going to perform, if you want to know how exactly this is done just keep watching. [MUSIC]