[MUSIC] So, let's move to the last CTL operator which we want to discuss, the always operator. So, if we want to compute the satisfaction set for a CTL formula that involves the always operator, like here for example, exists always phi. This translates to computing the greatest set V of states, such that V is a subset of the set of states that are phi states, and for which the set of successors, the union of the set of successors and V is non-empty. What does it mean? Well, it means that V is a subset of the set of states that have a successor in V. Also, for the always operator, we can formulate a fixed point characterization. And here, V is the satisfaction set we want to compute and it's again a fixed point of such a higher order function omega, and omega in this case is given by the set of states that are phi states. So they're in the satisfaction set of phi and the union of successes of S and V is non-empty. So how do we go ahead about the computation? Let's compute the satisfaction set as the largest subset V of the state space such that well, first of all, V is a subset of the satisfaction set of phi. And, this makes perfect sense because we want to check that always phi. So, only states that are in the satisfaction set of phi are possible candidates. Then, second s, if s is in V, this implies that s has a successor in V. Yeah, and this is this part again. So, we start our computation, again, an iterative computation with S0. And S0 is the satisfaction set of phi, because of 1 here. And now, we iteratively decrease this set by removing all states that do not have a successor in V. So, let me visualize this for you. We start with the set S0 and in the next iteration, we decrease this set to S1 and we remove such a state that only has successors outside of S0. And again, we keep doing that until we've reached the fix point of this iteration. So, we do this until the set does not change anymore. So, let me clean this picture up for you. As you see, I remove all the states that don't have a successor here in V. And what we do with this is, we iteratively now decrease the set, the computation set until we have computed the satisfactions set exist always phi, as we want it to, of course. Let's take a look at an example. This is an example with eight states, and we want to compute the satisfaction set for exist always b. So, only b states are candidates now. And, as you can see, we have one state that is a b state, but it does not have a successor in this set of b states, so the only successor was out here. So, this state needs to be removed so now, we have a computation set with three states. And if you want to decrease this even further, you see that it's not possible, because all these b states have a successor in themselves. So we're done, we've reached the fixed point of this computation and the satisfaction set is given by these three states, yeah? So, this was an example of computing exist always, and now you know how to do this for always and for until we can fill the gaps in the recursive computation procedure for the satisfaction sets. Right, here the upper three you already did see. So these you already did see. Exists phi1 until phi2, I've explained in the previous lecture. This is the smallest set T, such that the satisfaction set of phi1 is a subset of T. And if s is in the satisfaction set, and the union of the successor set in T is none-empty, then S is in T and this should be a small s, I'm sorry for this. Okay and then, we have the satisfaction set of exist always phi and this you've just seen, it is the greatest set V of states. Such that V is a subset of the satisfaction set of phi and S is in V implies that S has a successor in V, right? So with this, and the knowledge that every CTL formula can be rewritten in existential normal form, you have all the means to compute the satisfaction set for a CTL formula. While in practice, it might be a bit cumbersome to rewrite every CTL formula in existential normal form, so I will just briefly show you how these algorithms change when you allow the universe quantifier instead. So, if we want to compute the satisfaction set for all next a, this is almost the same. What you have to do now is you have to compute the set of states for which the set of successors is now a subset of the satisfaction set of a. And you see the difference, right? If we had the exist quantifier, we always needed to ensure that the set of successors and the satisfaction set of a was non-empty. So the option stated to there exists one path. Now, we need to ensure that for all the path, this holds. So, we have to ensure that the set of successors is a subset of the satisfactions set. That means basically, that all the successors are in the satisfaction set. Now, how for always a? This again, can be formulated as the greatest set T of states and here, it's basically the same idea, T is a subset of the states s, that are in the satisfaction set of a. And again here the successors of s are a subset of T. And the same thing as before, we need to ensure that this holds for all the successors. The same idea for the satisfaction set for all a until b. This again, is the smallest set T of states such that, here we have the union of the satisfaction set of b and here, all states s that are in the satisfaction set of a and the set of successors Post(s) is a subset of T, right? So this is the only thing you need to change. Wherefore exist, you had to check whether the set of successors and some satisfaction set, or some V was non-empty. Here, you always have to check that all the successors fulfill the requirements you have. So now, you also know how to model check universally quantified formulas. Now, if you want to learn more about CTL, maybe about the complexity of CTL or the relationship between CTL and LTL, I would like to recommend this book to you. It is called Principles of Model Checking and it is written by Christel Baier and Joost-Pieter Katoen and it has basically, it has all the things you ever wanted to know about CTL and LTL. [MUSIC]