0:04

Welcome again. In this lecture,

Â I will introduce Boolean equation systems,

Â which are the workhorse to determine whether

Â a modal formula is valid on a labeled transition system.

Â So, let's look at this labeled transition system

Â with two states and three transitions, labeled it an a,

Â a b and a c. And take this as

Â an example on which we want to verify a particular modal formula.

Â And for the modal formula,

Â we take a rather arbitrary one,

Â but one that you already know, namely,

Â the formula that says that whenever we can do an a,

Â then a b will absolutely follow.

Â And that's this formula.

Â So this [true* a] and then this typical minimal fixed

Â point formula that negate B.

Â If you want to solve this,

Â then one technique is to translate

Â the modal formula and labeled transition system to a Boolean equation.

Â So let's ask ourselves what a Boolean equation is.

Â So a single Boolean equation is this one,

Â where we have X as a Boolean variable â€“ that variable can be either true or false.

Â You have is phi.

Â Phi is an Boolean expression without negation,

Â and mu is the minimal fixed point operator.

Â So we are interested in a minimal Boolean value for X,

Â such that X is equal to phi.

Â And we also have a maximal fixed point operator,

Â so we can also write mu X is equal to phi.

Â And phi is typically true,

Â false, X itself, the and or the or.

Â And we cannot use negation the right-hand side

Â because then the formulas would not be monotonic anymore.

Â We are particularly interested in sequences of Boolean equations.

Â And I'm using the word sequence on purpose and not

Â set because the order of these Boolean equations is important.

Â So a typical example is this one,

Â where we have two equations: mu X is X or Y,

Â and mu Y is X and Y.

Â If you look at a Boolean equation,

Â then we can ask ourselves what the solution is.

Â So, mu X is X has two solutions,

Â namely, x is equal to true and x is equal to false.

Â And what we do is,

Â due to this minimal fixed point operator,

Â is that we select the minimal solution.

Â And if we would write the same with the maximal fixed point operator,

Â and what we see is a nu X is equal to X.

Â And we select this solution,

Â X is equal to true.

Â If we take more complex sets then we can follow the semantics of the solution.

Â There's only one single solution for this Boolean equation systems.

Â And as an illustration,

Â I will follow the definition of the semantics,

Â but this is a somewhat cumbersome procedure and,

Â therefore, it's not really practical to solve these Boolean equation systems.

Â But let's simply do it.

Â So, the semantic says that we have two options for X in this Boolean equation system,

Â namely X is false and X is true, that we can try.

Â And we will simply try to figure out whether X is false and X is true are solutions.

Â Now, if you go to left side,

Â then X is equal to false can be used to simply find equations.

Â So we replace X by false,

Â and then we get mu X is equal to false or Y.

Â And if you even simplify find the second one,

Â then we get nu Y is equal to false.

Â And then we can see that there's only one solution for Y.

Â We can substitute that solution for Y in the first equation,

Â and we see that X is false is also a solution,

Â that X becomes false,

Â and that shows that X is false is a solution.

Â In the same way we can do this for in the case where X is equal to true.

Â So, we substitute X is equal to true in the equations and we get

Â these two new expressions.

Â And we see in particular that we have nu Y is equal to Y.

Â And we know there are two solutions for Y.

Â But due to the maximal fixed point operator,

Â we have to select the maximal one.

Â So Y is equal to true is the solution for the second equation.

Â And then we substitute that back.

Â In the first equation,

Â we see that X is equal to true,

Â and that means that X is equal to true is still a solution of this equation.

Â So we have X is false being a solution,

Â X is true being a solution.

Â And now this minimal fixed point operator kicks in and it

Â selects the minimal solution of the two.

Â So what we do is we take X is equal to false,

Â and as a consequence Y is equal to false,

Â and that's the solution for this set of two Boolean equation systems.

Â Typically, we encounter Boolean equation systems of

Â hundreds of thousands or even many millions of equations.

Â Now, let's ask ourselves how we can use

Â these Boolean equation systems to solve this modal formula.

Â So, what do we do?

Â Let's copy it to the next slide.

Â Oh, let's first eliminate the regular formulas.

Â So the first, true* is being replaced by this maximal fixed point operator.

Â And let's now take this new modal formula to

Â next slide and let's try to solve this.

Â In order to solve this,

Â I want to give a name to both states.

Â So here we have state s_1;

Â here we have state s_two.

Â And I want to introduce four variables,

Â Y_1, Y_2, X_1 and X_2.

Â And Y_1 means that the formulas starting with nu Y is valid in state one,

Â Y_2 means the formula starting with nu Y is valid in state 2.

Â And the same holds for X_1 and X_2, namely,

Â X_1 means the formula starting with mu X is valid in state 1,

Â and the formula starting with mu â€“ and X_2

Â means the formula starting with mu X is valid in state two.

Â So, how does this look like?

Â Well, we get four equations,

Â and the fixed point operator for Y carries over to Y_1 and Y_2,

Â and the fixed point operator for mu carries over to X_1 and X_2.

Â And if you look at Y_1,

Â then the question is,

Â what is the shape of the right-hand side?

Â And this follows the modal formula.

Â So let's look at the first part of the modal formula.

Â And this says that whenever I am in a state,

Â whenever I can do an action in that state,

Â Y should hold in the resulting state.

Â So in state s_1, I can only do an a and end up in state s_2.

Â So, for this to be valid,

Â Y should be valid in s_2,

Â so the right-hand side of the first equation should become Y_2.

Â And now we can look at the second part of this equation.

Â So this says whenever we can do an a transition in state s_1,

Â mu X should become valid in s_1.

Â So, in s_2, sorry.

Â So, X_2 should be valid.

Â So what we see is that in the right-hand side,

Â we require that X_2 is valid.

Â And this is the whole equation that results when trying

Â to verify to see that Y holds in s_1.

Â Now let's look what happens if Y_2... of what's necessary to make Y_2 valid in state s_2.

Â So, if you look at the first part of the formula again,

Â then we have to look at any outgoing transition from s_2.

Â So, b and c. So,

Â first let's look at b.

Â And after doing b,

Â formula Y should be valid in state s_1.

Â So this gives rise to the following part of the modal formula

Â of the Boolean equation system, Y_1.

Â And if we do that, see,

Â see that we end up in s_2,

Â and Y should be valid in s_2.

Â So, here we get in the right-hand side Y_2.

Â Then we look at the second part of the formula.

Â So, whenever we do an a action in state s_2,

Â but we cannot do an a action,

Â well, something must hold.

Â As we cannot do this a action,

Â the resulting requirement is simply true.

Â Well, in this way, we can also give the rest.

Â So for X_2, it's actually that X_2 should be equal to X_1 and true.

Â And because X_1 does not occur in the right-hand side of any of the other equations,

Â we can simply ignore it.

Â Now the question is,

Â what's now the solution of this Boolean equation system?

Â I will deal with that in the next lecture.

Â But, for the moment,

Â I can say that solution is actually Y_1 is

Â equal to false and all the others are also equal to false.

Â So, given that Y_1 is equal to false,

Â we see that the formula is not valid in initial state,

Â and that's exactly what we already observed in the beginning,

Â namely that this formula does not hold for this transition system.

Â So let's look at an exercise.

Â We already saw that this particular formula that we were looking at was too

Â strict to express that b should follow a if c can come in between.

Â So we had this somewhat weakened formula that says that whenever we can do an a,

Â we will be able to do a b as long as no b is done.

Â And if you would apply exactly the same procedure to this formula,

Â on this transition system, the question is,

Â what is the boolean equation system that we will obtain?

Â So what did we show? We introduce the notion of a Boolean equation system as

Â sequences of simple Boolean equations with maximal and minimal fixed point operations.

Â And we sketched how a modal formula â€“ together,

Â with a transition system can be transformed to

Â a Boolean equation system such that the solution of the Boolean equation system is

Â exactly an indicator on whether the modal formula is valid for this transition system.

Â In the next lecture,

Â I want to explain how you can solve a Boolean equation system.

Â