[SOUND] So after two lectures of preliminaries, we can now try and model check our first CTL property together. This is the example property. It states that exist next A or exists B until not C. So first, we cut this formula into pieces, where we start with the highest binding operator and work our way down to the atomic properties. Then we rearrange the pieces to form the so-called path tree. And again, the highest binding operator forms the root of the path tree. Then we go ahead and do the model checking. And we start with the leaves of this path, parse tree, and that is here, A, B, and C. A, B, and C, and what do we do? Well, we compute the satisfaction sets for the property A, the property B, and the property C. Then we go one level up in this parse tree. Here, we have to check exist, next, A. And what we do is we re-label this, give it a new atomic property name, phi 1, and exist next, we've already discussed. We need to check whether the intersection of the set of successors and the satisfaction set of A is non empty. Then we proceed here with not C, or not the satisfaction set of not C is easy. It is the state space S without the satisfaction set of C. And then again, we can go one level up, and we do some re-labeling again, namely this B until not C is now labeled as phi 2. We don't know how to model check this one yet, but I'll explain in the future of course. Now, assume that you know how to compute this satisfaction set. Then we can go one level up again. And what we do is, since we have replaced these sub-formulas, let's call them a1 and a2. Now, we can check the whole formula by checking whether a1 or a2, and this corresponds to that note in the parse tree. So take a look again at what we did. Computed the satisfaction sets for the leaves and then went one level up and applied the rules for computing the next higher satisfaction set. Now, let's come back to this original question on how to model check arbitrary CTL formulas. Given the label transition system T and the CTL formula phi, the question is, does this tradition system T satisfy phi? How do we do that? Well, we compute the satisfaction sets in a bottom up way for all sub-formulas and then compute the satisfaction sets on the next higher level as I've illustrated to you. So you compute the satisfaction set psi as all states from the state space that fulfill psi here. And what I'm going to show you is the computation for CTL formulas in the so-called existential normal form. That limits the operators that we can use, but it doesn't limit the expressivity of CTL. So it's not a limitation in that sense. And, analogously to those algorithms I'll show you, you can design CTL model checking algorithms for those operators that I did not show you. But it is really not a limitation to restrict ourselves to this existential normal form because each CTL formula can be rewritten in an equivalent formula in the existential normal form. So, what does this mean? Well, in CTL formula in the existential normal form only uses these modalities exists next, exists until, and exist always. So how do we do that? A CTL formula in the existential normal form consists of these operators. So true, anatomic property a, not psi, psi1 and psi2, exist an x phi, exist psi1 until psi2, and the last one is exist always psi. So that is the operators you can use, and what you need to know is that if you want to express a CTL formula using the always operator, always next phi. You can rewrite that as not exists next not phi. And then you have an equivalent CTL formula in the existential normal form. And the same for all phi 1 until phi 2, you rewrite that, it's a little bit more complex, but it's possible. So it rewrites to not exist. And then in brackets, not phi 2 until not phi 1 and phi 2 and not exist, always not phi two. So, this is a little bit complex, but the good news is you do not have to do this. It's just important to know that each CTL formula can be rewritten as a CTL formula in the existential normal form. So with this knowledge, we can restrict the number of algorithms that are formally introduced to you. One little thing, here, it reads, not exists, and then in brackets, not phi 2. So you might recall that I stated earlier that something like not exists, not phi is not a CTL formula. Well, yes, because this not is a state formula. But here, the thing is, We have an until formula wrapped inside the exists operator, and then this until consists of a two state formula. So not phi2 and this one, and now you cannot read anything anymore, [LAUGH] but I hope that you got the point I tried to bring across. So if we are able to express all CTL formulas in the existential normal form, then we can use the recursive computation of the satisfaction sets as is on this slide. So the satisfaction set of true is just the whole state space. The satisfaction set of an atomic property a is all the states in the state space that are in the labeling of a. Then the negation is just the state space without the satisfaction set of psi here and is the intersection, again, of the two satisfaction sets for phi1 and phi2 and the satisfaction set of next exist, next 5. Again, is here the intersection of the set of successors of s and the satisfaction set of phi, and it has to be non empty. And then there are two more, namely, exist with an until and exist with always. And these two are more complicated, so in the next lecture, I'll explain to you how to model check this one, and in the last lecture, you will see how this one is model checked. [SOUND]