[MUSIC] So now, we want to see how we can possibly model check the CTL until operator. Well, first of all, we need to realize that exists phi 1 until phi 2 is the same as saying phi 2 holds immediately or phi 1 holds and there exists, next state for which there exist a path such that phi 1 until phi 2. Yes, this is an expansion for exist until which allows us to compute the satisfaction set as the union of the satisfaction set for phi 2 because in all phi 2 states the formula is immediately valid. And the set of states that are in the satisfaction set of phi 1 and for which the intersection of all successor stage of s and the satisfaction set of exist phi 1, until phi 2 is non-empty. Now, this in turn, can be expressed as a fixed point characterization of the satisfaction set for exist until. And what do we do? Well, this set T which is the satisfaction set of exists phi 1 until phi 2 is a fixed point of the higher-order function omega which assigns from 2 to the power of s to 2 to the power of s. So it says something about the validity of this formula for each set in the satisfaction set. And this is the function omega, so it is the satisfaction sat of phi 2 and the union of all states s that are in the satisfaction sat of phi 1 for which the set of the successors with the union of T is non-empty. So what we're looking for is a fixed point solution of this function omega, and such a solution fulfills two requirements. And the first one is that the satisfaction set of phi 2 is a part of this satisfaction set we're looking for. And then the other one is that if a state s is in the satisfactory set of phi 1 and the intersection of the post successor, and the satisfaction set we're looking for is non-empty then it follows that this state s is in the satisfaction set of exists phi 1 until phi 2. Now, let's do this. So the satisfaction sat exists phi 1 until phi 2 can be expressed as the smallest subset T which is subset of S. [LAUGH] Such that on the one hand here the satisfaction set of phi 2 is a subset of T, and on the other hand if s is in the satisfaction set of phi 1, and again, the successors of s, in a intersection with T, is non-emptied, then it follows that s is in this T. So, we start this iterative process which leads us to the fixed point solution, with an initial set S0 which is just the satisfaction set of phi 2. Why is that? Because all phi 2 states immediately fulfill this formula. Then in the next step we compute what we call S1 and this is the union of S0 and all phi 1 states that can directly move to S0. So let me illustrate this for you, we start with S0 which is the satisfaction set of phi 2, and then we gradually increase the set and then here we have S1, and how do we increase it? Well, we add all states that have here a successor in S0. Now we do this one more time in here, so then we increase again, and we have S2. And again, we add all states that can directly move to the previous set we have computed. We keep doing that until the set doesn't change any more. So that is when we've reached the fixed point. So let me clean this picture up for you. This is a bit nicer. So what we do is we iteratively increase this computation set until we have reached the fixed point. And this fixed point immediately is the satisfaction set we are looking for. So this what we wanted to compute actually. So let us take a look at an example. This is a simple labelled transition system. It has four states, as you can see. Two are yellow, one is blue. And the one behind me is just black, and you do not need to try the computation. So what we do is we want to compute the satisfaction set exist yellow until blue. So in the first iteration we start with the satisfaction set of blue. This is only one state. So this is the first iteration and the states that are depicted green now are in the computation set. Then, for the next iteration, we add all states that are yellow and that can directly reach a green state, right? So this is that one state which we need to add. And then in the next iteration, well, we add the last yellow state because it can now reach a green state. If we keep going you see that there's nothing to add anymore. So now, the green states here, they form the satisfaction set of exists yellow until blue. This is how to model check the exist until operator in CTL, and if you're interested in the always operator, I recommend that you watch the last lecture of this module. [MUSIC]