Welcome. In this lecture, I want to show you Gaussian elimination as a simple technique to solve Boolean equation systems. So if you have Boolean equation systems, then the question is how can we systematically solve that? And if they are relatively small, then there's a very elegant method - and that's called Gaussian elimination. And Gaussian elimination got this name after Carl Friedrich Gauss, who invented this rather famous method to solve linear sets of equations in number theory. And because our method somewhat resembles this approach, we also call this Gaussian elimination to solve Boolean equation systems. What's the idea of Boolean - of Gauss elimination? Well, there are three rather simple rules and I will explain these rules. So the first rule is called variable elimination. If you have a single equation of the shape nu X is phi, then we can replace it by this equation, where you place every occurrence of X in the right-hand side by true. So all the occurrences of X in the right-hand side are removed in this way. And the fact that we take true is directly related to the maximal fixed point. If you have a minimal fixed point equation, then we replace X by false. And this can always be applied at - in a Boolean equation system, but we will specifically apply it at the last rule of the Boolean equation system. So let's take our example. And let's look at the last creation. It says mu Y is equal to X or Y. And now, because it's a minimal fixed point operator, we can replace Y in the right-hand side by false. So what we obtain is this. And then you can simplify the equation a little bit. And this is what we have. In particular, note that Y does not occur anymore in the right-hand side of this last equation. Now, look at the second rule. That's called backward substitution. So if you have a sequence of Boolean equations - and here the sigmas indicate either mu or nu, so we can do it with arbitrary fixed-point operators. And we look at the last equation. Then this says sigma Y is equal to phi. And what we can do is we can substitute the phi for Y in all earlier equations. And this is what we obtain. And what we see is that we remove Y from all earlier - all earlier equations. So if we apply this to our example, the last equation says mu Y is X - and now we can replace every occurrence of Y in the early equations by X. So we obtain this equation - nu X is equal to X and X. We now forget about the last equation, because Y does not occur anywhere anymore in our Boolean equation system. And what we have done now is that we removed all occurrences of Y and we actually obtained a really smaller equation system. And what we can do is repeat this procedure until we only have one equation left, namely the first equation - and have a right-hand side that is equal to true or false. And then we know the solution for the first variable of our Boolean equation system. But first, let's simplify this equation. So we get nu X is X as the first equation. And we can then apply variable equation - variable elimination to the first equation. So we have nu X is X. And because it's a maximal fixed point operator, we can replace by nu X is true. And we know the solution for the first equation of our Boolean equation system. Now we have the third rule, that forward substitution. And we can only apply forward substitution if the right-hand side of the equation that we use for substitution does not contain variables. So let's look at the general scheme. Here we again have a sequence of Boolean equations. We have these minimal and maximal fixed point operators in sigmas - indicated by sigmas. And if phi does not contain variables, so it's effectively equal to true or false, then we can substitute this true or false for all occurrences of Y elsewhere. So let's apply that to our example. We have nu X is equal to true. And because the right-hand side does not contain variables, we can substitute true for X in all later equations. Well, that's only one in this case. But we simply obtain X is equal to true and Y is equal to true as the solution for our Boolean equation system. And what we have seen is a very general method. This works for all Boolean equation systems. I mentioned that the order of Boolean equations is important for the outcome. So what we can do is we can take two Boolean equation systems with exactly the same equations, but the order of the equations is different. And we can try to solve both sets and see that the answers are different. So let's look at the first equation system. The second equation already does not have a Y in its right-hand side, so we do not have to apply variable elimination, but we can immediately apply backward substitution. And what we obtain is, as first equation, nu X is equal to X and X. And because the first equation is a maximal fixed-point equation, we can use variable substitution and replace X by true and we obtain nu X is equal to true. And if we then do forward substitution, we obtain mu Y is equal to true. And we have solved this Boolean equation system. Let's now also solve the second Boolean equation system. So we first apply variable elimination on the second equation. We still have an X in the right-hand side and replace it by true. We then substitute the Y and we simplify the equation. And we - so we get nu X is Y and we substitute Y for X in the first equation. And we can now apply variable elimination to the first equation. And now we have solved the first equation. Do forward substitution, and we obtain, as a solution, Y is equal to false and X is equal to false. So if you look at this solution - and we look at this solution, I think it's completely obvious that sequence in which the variables occur do matter for the solution that we obtain. So one of the questions is how efficient Gaussian elimination is. And although it looks quite straightforward, the procedure is still exponential, although it's quite hard to figure out why that is the case. Actually, the situation around solving Boolean equation systems is quite weird. So for that, we have to understand that solving a Boolean equation system is in NP and in co-NP. So problems in NP are those problems where, if you can give an answer yes to an instance of such a problem, then you can check that in polynomial time. So calculating it might be hard, but checking that the answer is correct might be easy. And problems in co-NP are those problems where if the answer is no, you can check that easily. And there's a big subclass of these problems and that are those problems that you can simply solve in polynomial time. So you can then also check whether the answer is yes or no. And that's both in NP and in co-NP. What we see here is that there is an area above this red area, this triangle - and that are those problems that are in NP and in co-NP, but do not have a - a polynomial algorithm. And what is commonly believed is that there are no problems in this area. So for a long time, it was believed that primality testing was in this area, so it was in co-NP and it was in NP and no polynomial algorithm had been found. But ultimately, people came up with polynomial algorithm. As it appears now, solving a Boolean equation system is in NP, it is in co-NP and we still do not have a polynomial algorithm for it. And this causes a lot of people to believe that we should be able to find this polynomial algorithm, although I spoke to a few colleagues that said that they were giving up on this because it's so hard to find one. Let's look at exercises. In a previous lecture, we had this formula. And the question was how does the Boolean equation system look like to verify this formula on the given transition system? And the answer was this. And now the question is can you solve this Boolean equation system? And how does the solution look like? So what did we do? We introduced Gaussian elimination as a set of three simple rules to solve Boolean equation systems. And Gaussian elimination is fairly useful to solve simple Boolean equations - equation systems. We showed that the order of equations in a Boolean equation systems is of importance for the solution. And we also shortly hinted that it's still an open question to find a polynomial algorithm to solve Boolean equation systems in general. Fortunately, for all those Boolean equation systems that we generate for our practical applications, there are efficient algorithms and we can solve them quite quickly. So we are now at the end of the third MOOC, where we looked at modal formulas to express requirements on behavior of systems. In the next MOOC, we will deal with application of everything we learned to a whole range of examples. I hope you enjoyed what I told you and I really hope to see you in the next MOOC.