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.