[MUSIC] In this lecture, we will see how we can formulate fairness properties using alternating fixed point operators. You may not realize it, but we have already seen several formulas where we use minimal fixed point operators and maximal fixed point operators at the same time. An example is this one, namely, the formula that sets when a fire breaks out, there is the possibility of the fire workers, the firefighters to appear. And the second part of this formula is actually minimal fixed points. And the first part of this formula is a maximal fixed point operator. But what we do not see here is that the fixed points alternate, so first you basically use the maximal fixed point, and if the fire action happens, you go to the minimal fixed points, and they are not actually nested. But if you nest these fixed point operators, then you can formulate fairness properties. And fairness properties are properties that holds when certain actions do not happen infinitely often. So that's what I just indicated. So, let's just look at two examples. This is the first example, and this is a formula that holds on trace of a's. So you can see the two fixed point operators, and then whenever an a happens, you either go to X in the first part, or you go to Y in the second part. And in the first part, you select the first part, if you came to a b-action. And if in a particular state, a b-action is not possible, you iterate to the y and you select the second part. So, let's look what this actually means, so if we have this sequence of a's, then we have some states with outgoing a's, b's. And now, what the formula says is that when we iterate through the X, we cause the rb's in these initial two states, then we can only iterate through this X finitely often, because the X is preceded by a minimal fixed point operator. If we, so this means the number of b's should be finite. If we then look at the next states, we cannot do these b's and we iterate to the Y, and the Y is proceeded by a maximal fixed point operator. So, we can actually do this infinitely often, but if it happens, as it is shown here, that after a number of times a b happens again in the state, then we iterate again through the X, and the X says that this can happen only a finite number of times, so we have to enter at stage where we cannot do a b. And because the minimal fixed point is in front, we actually state that the total number of b's that we can do is finite. So, what this says, is that we iterate to X and these two states, we iterate through Y in these states, to X again in these states, and Y here. And we can only, a cycle finitely often through the X, so what we state is that if you have such an a-trace we can only have a finite number of states with an outgoing b. Now, we can look at the same formula, and change the fixed point operators in front of it. So, we move the mu Y to the front, and we put mu X at second place. So remove the old formula, we consider this formula. And we look at the same sequence of a's, and if we now figure out what is happening, then we see that in the first stage, we iterate with X and we can only do that finitely often because it is proceeded by a minimal fixed point operator. So after a finite number, we have to end up in this state where we iterate toward Y. And that is what we can do infinitely often, but supposed we end up again at a state with an outgoing b. Then what happens is that the counter of the X is reset, and we can again have a finite sequence of states with outgoing leash. And that is typically what happens here. So we can cycle finitely often through the X. When we cycle through the Y, we reset the x, and that means that we now state with this formula that every subsequence of states with an outgoing b should be finite. But we can have an infinite number of states with b's, as long as each subsequence is finite. So what we can ask ourselves is the following, can we find a transition system that is true for the formula P2, that was the last one I just showed. And that is false for the first one, P1, so how can we do that? Well, P1 said that we only allow a finite number of states with an outgoing b, so we have to invent something with an infinite number of states with outgoing b's. P2 says that only, that each stretch of b's should be finite. So what we can do is we select a state at an outgoing b, we take a finite stretch of these states. So, the next state we do not have an outgoing b, but one a step later, we have this outgoing b again. And we simply alternate which states with an outgoing b and without an outgoing b. In this way, we can actually make this, formulate this in a fairly compact transition system like this. And what we see is that this transition system is not valid, or that phi 1 is not valid for this transition system, and that phi 2 is actually valid, so this is a formula that distinguishes between these two. And this shows the subtle difference between changing the fixed point operators. There is no counter example where phi-1, for a full reach phi-1 is valid and phi-2 is not valid. So, let's go to an example that we saw the previous time, namely this example that says that whenever an a happens, then b must unavoidably happen. So along every trace after a finite number of steps, we will see that the b must happen. And what we probably recall is, if you had this example, where we do this a, followed by the b, but it could be that such an action c would come in between infinitely often. And we saw how to deal with this. But if we would formulate it very precisely that after the a, the b must happen within a finite number of steps except that only the action c can come infinitely often in between, we have to use alternating fixed point operators. So, this is what we want to say. We want now to say that whenever a happens, b must happen, except that c can happen infinitely often in-between. So, we start with the same initial part of the formula, so whenever a happens, then, and we now use a minimal fixed point in the same way as above, but we add this maximal fixed point and we say, whenever the c happens, we go, we iterate through the maximal fixed point, so this expresses that we can, we allow c to happen infinitely often. And we say that whenever something else than b and c happens, we must iterate finitely often, so this guarantees that a b will happen within the finite number of steps, except then for the c. And we have to add this last part, true true, to guarantee that we do not end in a state without outgoing transitions, but this guarantees that we end up in a state. Now we only have outgoing b's. Okay, this is what I wanted to say about the alternating fixed point operators. So, let's change the order of the fixed point operators again a little bit. So this is a formula that you have not yet seen. And the question is, what does it express? The second exercise- If we are studying data transfer protocols, then we want to deliver data. Except that if data is always lost in transmission, then we cannot deliver data. So, what we want to state is that if data is not infinitely often lost, then arrive will happen along every conceivable path. And how do we formulate it? So what did we see? We saw that we can use alternating fixed points to express fairness properties. And these formulas can be fairly complicated. Fortunately, I've hardly seen formulas where you have three alternating fixed points, and four or more alternating fixed points are really not occurring that often. In the next lecture, we will see how we can formulate the correctness of Peterson's mutual exclusion algorithm using model formulas. Thank you for watching. [MUSIC]