[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. 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. 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. In this expression, we have X plus abY, and we see that we can do X before having to do an action, and here X is not guarded. 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. 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. 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. So, that's what we can conclude here. 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. 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? Look at the six recursive specifications. 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. Thank you for watching. In the next lecture, we will extend our capacities to specify interesting behavior even more by adding data to our specifications. [MUSIC]