0:00

[MUSIC]

Â Welcome again.

Â Up 'til now we have seen process expressions with which we can only specify

Â behavior that is finite, so we can only do a finite number of actions in sequence.

Â In this lecture, we will see how we can use recursive specifications

Â to specify infinite behavior.

Â With label systems we can easily specify the behavior of this a machine,

Â which can infinitely often do an a in sequence, and

Â up 'til now, with our posted expressions, we cannot specify that.

Â And we use recursive equations to specify these.

Â So, what's a recursive process specification?

Â It's essentially the following; that you have an equation of

Â the following shape, namely, with a process variable at the left,

Â and a process expression at the right.

Â So typical examples are these: for instance, x is ax,

Â and this specifies the process where you can do an a, and then afterwards,

Â you can do the behavior of x.

Â And x, of course, can do an a again, so this exactly specifies the behavior,

Â or process, that can do an a indefinitely.

Â We can make this process, expressions,

Â at the right hand side also a little bit more complex.

Â So, look at this example here.

Â We have the equation y = a-b-Y+c-d-Y, and

Â this represents the behavior where you first have

Â a choice between ab, or a choice between cd.

Â And after doing the ab and the cd, you go back to the initial state,

Â where you have the choice again.

Â 1:54

You can also write down sets of such equations.

Â So here we have the behavior: U is aW, W is bU.

Â That, of course, represents this behavior.

Â We could easily write it down as one single equation,

Â but sometimes it's convenient to use more equations.

Â Okay, there is something quite important with recursive process specifications,

Â and that is that they must be guarded in order to define behavior.

Â And we call a process variable, guarded,

Â if it's proceeded by at least a single action, like this.

Â So, a is, in this case, the guard before X.

Â 2:40

And it can also occur in more complex expressions, so

Â here we have the guard a plus b, X and the guard bY.

Â But before we reach the variable, the process variable,

Â we at least have to pass through an action, that's the idea of a guard.

Â 3:14

We say that a recursive specification is guarded if all process

Â variables occurring in the right-hand side are actually guarded.

Â So typically, X is aX is a neatly guarded recursive specification.

Â X is aX plus bc plus dX is also nicely guarded.

Â But this process of this equation, Y is a plus abY has Y on the right hand side.

Â That is not preceded by an action, so it is not guarded.

Â 3:46

If we have guarded recursive specifications,

Â we can use the very important recursive specification principle.

Â And this principle says that if we have a guarded recursive specification,

Â it has (at most) one solution.

Â Guarded recursive specification always have solutions.

Â So it actually says that it has exactly one solution.

Â So how can we use this?

Â Well, for instance, as follows.

Â If we have these two process equations, X is aX, and Y is aaY,

Â then we can already see or feel that X and

Â Y represent the behavior that you can do a indefinitely.

Â So that means X and Y should be strongly bi-similar and

Â we would like to be able to prove them equal.

Â 4:37

And the ID is now the following, that we find a guarded recursive

Â specification to which X and Y are both a solution, because this guarded

Â recursive specification has only one solution, X and Y must be the same.

Â So in this particular case, we can derive that X is aaX.

Â Take the equation, X is aX, and replace the X in the right

Â hand side by aX because we know that X is equal to aX, and we get this equation.

Â And now we see that X and Y satisfy exactly the same recursive equation,

Â guarded recursive equation, and that means that X and Y must be the same.

Â They are characterized in the same way.

Â 5:32

Just as an illustration, we prove

Â that X and Y defined by X is aX and

Â Y is aY delta actually represents the same behavior.

Â And you can already feel that X should be equal to

Â Y because the delta after the Y cannot be reached.

Â So, the behavior of Y is essentially doing an a,

Â and then again an a, and it will never terminate.

Â How to prove that precisely?

Â Well, that's done as follows.

Â First, we observe that the Y delta is a solution for

Â Y in the equation of Y is aY delta, and this is seen as follows.

Â Y delta, and now we use the definition of Y,

Â is equal to aY delta followed by delta.

Â 6:26

We would like to put the brackets a little bit different, so use the action A5.

Â And then we get aY delta followed by delta, and

Â you can see that this is exactly the definition of the equation for

Â Y, where we replace Y by Y delta.

Â And we see that Y delta, is solution of exactly the same equation as Y.

Â And therefore, we can conclude with RSP that Y delta is equal to Y.

Â So we have not yet finished this proof.

Â Because we still have to prove that X is equal to Y, but that's now quite simple.

Â Namely, we know by the definition of Y that Y is equal to aY delta.

Â We know that Y delta is equal to Y, so

Â we know that Y is equal to aY, and now we see that X and

Â Y satisfy exactly the same guarded recursive equations,

Â and that means that X and Y must be equal by RSP.

Â Okay, let's do a few exercises.

Â So if we have the behavior Y is a plus bY plus b,

Â what's the corresponding transition system belonging to Y?

Â 7:55

Which one of the six are guarded and which are not?

Â And for the third exercise, let's look at these two equations.

Â X is aX and Y is aYb.

Â Can you prove, using RSP, that X is equal to Y?

Â So what do we see?

Â We saw that using guarded recursive equation to our guarded recursive

Â specifications, we can actually specify repeated behavior.

Â And using the principle RSP, we can prove processes defined by

Â guarded recursive equations equal to each other.

Â