[MUSIC] Welcome. In this lecture, I will show you the basic axioms for behavior. We know that processes can be equal in the sense of trace or strong bisimulations. So if we look at these two labeled representation systems then we see the behavior where we can do an ab. And we see the behavior where we have the choice between an ab and an ab. And that's not a real choice, so these are equal. And that means that they should also be equal if we look at them from the perspective of process expressions. So if you write down ab + ab, then that should be equal to ab. And the same way, if we have the behavior where we have an a or a b, or a b or an a, then we also want this to be equal. And the more complex expression is this one. The choice between the a and the b is made with the first action. So if you have a + b followed by c, then that's really the same as ac or bc. Question is, now how can we characterize that in a neat way for process expressions? And that can be done by axioms. And we have five basic axioms that characterize strong bisimulations and that are the basic actions for behavior. So the first axiom is A1 and it's called commutativity and it says that a choice between the processes x and y. And we use the variables x and y to characterize processes here. The choice that the sequences really doesn't matter so we can write x + y or y + x. The x represents strong bisimulation when we speak about axioms we have a tendency to write the equality sign, but we have to indicate which equivalence is meant with this sign. The second axiom is called Associativity, Associativity of the +, and it says that if we have the choice between x, y and z, there is no preference for one of them and it doesn't matter how we put the brackets. And the Associativity Rule allows us to drop brackets. In particular, we can write x + y + z, as you see below, because it doesn't matter how we put the brackets, we can put them at left or at the right as indicated here. This is probably the most remarkable axiom, so if you have the choice between x and x, then there is no choice at all. So x + x is actually equal to x. The fourth axiom is Right Distributivity, and it says that if we have a choice between the behavior x + y followed by that z, then this is really the same as a choice between x z or y z. And then we have the last axiom, and that's the axiom that represents the Associativity of the Sequential Composition. If we have the expressions of the processes x, y and z following each other then it really doesn't matter where we put the brackets, first x is executed, then y and then z. Okay, now we have a very nice property about these axioms, namely that these axioms exactly characterize, and I state it here as a theorem. These axioms exactly characterize strong bisimulation for process expressions that you can express with actions, the choice operator and sequential composition operator. And it has two aspects, one is called soundness. Soundness means that whenever I derive something using these axioms, then the two process expressions will be improved equal or also equal in the sense of strong by bisimulation. And all the properties says that if I have two process expressions that are equal in a sense of strong bisimulation, then I can prove them equal using these axioms and these axioms only. Ok, so how do we use these axioms? Let's look at this example. I put a question mark above the equality sign to show that we want to prove this. And we simply start with the left hand side, which we write down here. So we have a + b followed by c followed by the choice between d and d. And we can already see that this choice between d and d is not a real choice. So using the axioms A3, we can replace d + d by d. And this is what we get. And now I find it important that the records are put at the right place, so using the axiom A5, I insert the brackets for the sequential composition, and with this last expression, I want to distribute the c over the a + b using right distribution. So we use the axiom A4, and we get the expression ac + bc followed by d. And this is almost what we want to have. We have to switch ac and bc and then we get the final result. So that can be done using the axiom A1. And we get bc + ac is equal to d. Now, you may have noticed that we did not write down left distributivity as an axiom in the five axioms. And the reason for that is that this axiom is not valid in strong bisimulation. And we already know why. Because this behavior where we do an a, followed by b + c, is not equal to this behavior where we have a choice between ab and ac. And why this was not the case was illustrated by the example of the dragon and the princess. For weak bisimulation, however, this is exactly the correct rising axiom in addition to the five others that we have already seen. So we have the following theorem, the axioms A1 up to A5 plus left distributivity is exactly sound and complete for trace equivalence. We had also seen this other constant, this delta constant or called deadlock or inaction. And for this constant we have to axioms, namely x + delta = x and this expresses that deadlock, cannot do anything. And also if you have this choice of x + deadlock, we can not chose for this deadlock and we are forced to do the x. And the second axiom says delta + x = delta. So delta cannot terminate. That means that he can never do the behavior that follows delta. And that means that he can as well leave it out. And then we have, again, this axiom. It's probably a little boring now, but if we have process expressions with actions. The sequential composition, the alternative composition. And that log, then the axioms A1 up until A7 exactly characterize strong bisimulation. And if we add left distribution, the axioms A1 up till A7 plus left distribution exactly characterize trace equivalence. Okay we have now a few exercises for which we do not have registered answers, you should try to with a pen and paper and this is a standard equation where you have to prove using the axioms that the left and right hand side are equal for strong bisimulation. Suppose that we have two process expressions that are not strongly bisimilar. For instance, a followed by b + c and the choice between ab and ac. Then we cannot prove them equal using the axioms for strong bisimulation. But the question here is, what is the proper reason why we cannot actually prove them equal? Well, this is a third exercise, which is little bit a tricky one. So suppose that we know that we have processes x and y and that a choice between x + y = delta. So essentially, you can see that x and y can do anything. Now prove, using the axioms and the fact that x + y = delta. There have x cannot do anything at all so x = delta. And this is the fourth exercise, so we have some notation that is sometimes useful. In that is that x is contained in the y and that means that x + y = y. So the behavior of x does not add anything to that of y. Now show that if x is contained in y and y is contained in x then x = y. Okay, what did we do? We saw these five basic axioms that characterize strong bisimulation. These are really the basic axioms for behavior. And we saw the two extra axioms that characterizes deadlock and inaction, and we saw that left distribution can never be used when we are working in the setting of strong bisimulation. But in a setting of trace equivalence, it's exactly the one that we have to add to the previous axioms to exactly characterize trace equivalence. Thank you for watching. In the next lecture, I will show you how you can specify recursive behavior using recursive specifications. [MUSIC]
