[MUSIC] Welcome again. In this lecture I will introduce the all important minimal and maximal fixed point operators. Here we see Hennessy-Milner logic. And we would like to extend this Hennessy-Milner logic now with two fixed point operators to make it dramatically more expressive. So we have this extension of the syntax where we have the minimal fixed point operator which we generally write using the Greek letter mu. We have a maximal fixed point operator which we write using the Greek letter nu. And here we should see this x as a set of states. So what's the meaning of such a formula? Well, if you have the formula x and s, or x is found within s, if s is part of the set x. If we have a minimal fixed point operator, then this formula is found wihtin s. If s is part of the set x and x is the smallest set satisfying the equation x=phi. And note that x may occur in phi. And the same holds for the maximal fixed point operator, with one exception. That x is now the largest set of states satisfying this equation. So if we look at the following transition system, then we can ask ourselves which of the two model formulas are valid and which are not in this state s? So we the minimal fixed point operator with the diamond modality ax and a maximal fixed point operator with the same formula. And the way to investigate this is the following. We can look at all potential sets of states for x, and look whether they satisfy this equation. So the equation where x is equal to diamond modality x. So let's do that systematically. x can either by the empty set or it can be the set that only the state s and that are only two potential candidates. And what we can do is we can try to figure out what the set of states is where diamond <a>X is valid. So if x corresponds to the empty set, then there is no state from which you can do an a step and end up in a state in the empty set. So what we see is that empty set corresponds to a diamond ax if x is empty. If x is equal to s, then we can see that we can do an a step in the state s and end up in s again. So we see that diamond a(x) corresponds to the set with exactly the element s. In particular, what we see is that the empty set and the state with set s are both solutions of this equation. And now we can look at the minimal fixed point operator and the maximal fixed point operator. We say that a minimal solution satisfies the equation with the minimal fixed point operator. And the maximal solution is the solution for the operator where we used the maximal fixed point operator. So the minimal solution corresponds to mu x ax. And what we can see is that s is not part of this set because it's empty. And that means that this formula is not valid in state s. The solution for the maximal fixed point is the set of state s. And what we see is that the maximal fix point formula is actually valid in s. Okay, let's do this again for even simpler formulas. So consider mux.x and nux.x and try to understand them with the same reasoning as before. Namely, we look at the equation x=x and what we realize is that any set of data satisfies this equation. It's totally trivial, x is x also for any set. In particular, what we see is that the minimal solution is then the empty set. And the maximal solution to this equation is a set of all states. And the minimal solution, the empty set, corresponds to the situation that the formula is not valid for any state. That's essentially the property of all, so what we see is that the formula, mux.x is equal to false, it's valid for a null state. And what we see is that the set of all states corresponds to the formula true. So nux.x=true. Let's look at another property of fixed point operator, so again, look at mu x phi and nu x phi. What we see is that we are interested in solutions for the equation x=phi. And mu x phi is the smallest solution and nu x phi is the largest solution. And what's completely self-evident is that the minimal set satisfying this equation is always smaller than the maximal solution. So if we have a state that satisfies the minimal solution, then it's also part of the maximal solution. So typically what we see Is that a minimal fixed point, a mu x phi always implies mu x phi. There's one important property to note because not all formulas are actually valid. So look at arbitrary formulas where sigma is e to the minimal fixed point or a maximal fixed point. We can only speak about minimal or maximal solutions. If phi is a monotonic operator, the expression phi does not make sense. When is phi monotonic? Well, if we take phi x, and we increase x, we add more sets to the set of state x, then the corresponding phi x should also become larger. And that's the property that these sets should have. This looks a little bit hard to check but actually there's a very easy way to check this. Namely, x should only occur in the scope of an even number of negations. Starting from the fixed point where x was defined. So typically we can look at a few examples. Here we have mux.x and we see no negations. In particular, there are zero negations for the usage of x compared to the definition. Here we see, and that's also correct, an even number of negations before x. And in this case we see an odd number of negations and this expression is not monotonic and doesn't make sense, so it cannot be written down. The theory does not apply to it at all. We can even have a little bit more complex examples where have multiple occurrences of x. As long as each occurrence of x has an even number of negations in front of it, it's safe. And negations can even occur in quite complex patterns but here we see again that x has two negations in front of it. This is an example where we only have one negation in front of x that is not monotonic and therefore is not allowed to be used Okay, We can look at solutions of fixed point operators in terms of the minimal set and the maximal set. But that's not always convenient in practice. It's more convenient to look at finite iteration and infinite iteration. So we have this minimal fixed point operator and this maximal fixed point operator that we have already seen, and this transition system. And typically, what we see is that if we have a minimal fixed point. Then this minimal fixed point becomes valid if we can make the formula at right valid if we only iterate a finite number of times through x. So in particular, if you look at this formula diamond ax, then we can see that if we start in state s. We do an a step and then we reach the state s again and we have to check x for s again. And this goes on indefinitely, so this will not become valid after finite number of steps. And therefore mu x diamond ax is not valid in s. For the maximal fixed point operator, it is allowed to iterate infinitely. So in this particular case, you can do an a step and end up in x and you have to check whether x is valid in s. And you will iterate this infinitely, but due to the maximal fixed point operator, this is actually allowed. Minimal fixed point operators are also associated with liveness properties. Liveness properties are properties that say that something good must happen within a finite number of steps. And here we have this formula, mu x diamond a x bar and b true. And this says that in order to make this formula true, either we have to do a b or we have to do an a after which we end up in a state where it should be valid again. And due to this minimal fixed point operator, we can only iterate this a a finite number of times. So let's look to a transition system, what is says is, well, assume that we would do an a. Then we end up in a state and we have to check again that x holds in this new state. And this can go on and on, but only for a finite number of steps. And after a finite number of steps, the other part of the formula should become true. So after a finite number of steps we should do this b. So what this formula expresses is that there is a trace of a's, a finite trace of a's, after which a b action happens. Okay, we have also another class of properties, so-called safety properties. Safety properties are properties that are expressing that something that cannot happen. And it says that on all reachable states, even if you go on indefinitely, this bad thing cannot occur. So therefore we use maximal fix point operators for safety properties. And in this particular case, what it says is that whenever we do an a step, we must go on and check x again for the resulting states. And at the same time we should be able to do a b. So let's look at the transition system. If you have a state, then this property is valid if we can do a b, so that's a requirement. And whenever we do an a, we should also be able to do a b in the resulting state because the formula has to hold in the resulting state also. And if you do another a, b must hold and then we do more a's. b should hold in the resulting states and this goes on and on and on. So in all resulting states that we can reach with a steps, we should be able to do with b. So each state reachable by a's must have an outgoing b transition. In the last lecture we saw dualities and we already announced that the minimal fixed point operator is a dual of the maximal fixed point operator. Well, that's formalized here. We can see that if you apply the negation to the maximal fixed point operator, we get the minimal fixed point operator. And we have to apply negation to the formula inside and we have to do something in addition, namely we have to replace every occurrence of x by not x. And the same holds if we apply negation to the minimal fix point operator, we have to apply negation to the formula. And we have to apply negation to each occurrence of x. Why can this be useful? Well, consider this formula. It's dual is this formula and that's the formula we saw in the previous slides and we expressed it after, every sequence of a's a b should be possible. But it could be that we are not understanding this last equation, or this last fixed point, this last formula sufficiently well. So it could be that we actually are wondering what this nu x box ax and diamond b true means. And we could rephrase it using these laws for duality to this formula with this negation. And what if we can then do is remove this negation and first try to understand this simpler formula. And this mu x, ax r b false formula expresses that after any sequence that expresses that there is a finite sequence of a's that ends in a state where no b can be done. So recall that b box b false means no b is possible. So this is what it expresses. Now if we negate this, after you've understood this, then we realize that this expresses that there is no finite a-trace after which no b can be done. Or in other words, after any sequence of a's, ab is possible and that's exactly what the formula at the left bottom describes. And such transformations can sometimes really help to get insight and confidence in the meaning of such formulas. Okay, let's look at an exercise. We want to express that every sequence of a's is finite and it's terminated with a b. Where they have only actions of only a's and b's in our transition system. So which of these four formulas does express this? Again, in a setting where we only have actions a's and b's, we can ask ourselves, can we write down a formula that says that a b action is not possible at all? Well, we can make plenty of exercises with these model formulas. But let's look at this one where we have the maximal fixed point operator, [a]X. And this is equivalent to one of these four. And then the last exercise we have this maximal fixed point operator, ax. What is it that this formula expresses? Okay, so what did we do? We extended Hennessy-Milner logic with a minimal and maximal fixed point operator. And this really made a huge difference in expressivity. All of a sudden we can express, basically, everything that we can think of. This new language is called the modal mu-calculus. Minimal fixed points should be associated with finite iterations or with liveness properties. And maximal fixed points typically corresponds to infinitely repeating actions or safety properties. We've seen these minimal and maximal fixed point operators and it's quite tricky to express properties with them. So in the next lecture, I will introduce regular formulas which are far more convenient. [MUSIC]