[MUSIC] [SOUND]. Good to see you again. This time I will speak about the hiding operator and a little bit about the blocking and renaming operator. So let's look back at example from the previous lecture. Where we had this process ab in parallel with cd, and these represented buffers where you communicated bc into e. So, if we look at the behavior then we see that it starts with an a which is important to read information. Then we have this somewhat internal and irrelevant action where you simply communicate behavior from one buffer to another, and then you have to again import into d where you deliver the data. So what you would like to do is to hide the e, like this. And in the transition system it means that we replaced action e by Tau, so if you have done this we can apply branching bisimulation reduction and simply reduce the behavior to a followed by d. Now how can we achieve this in a process expression? Well, rather straightforwardly by applying the hiding operator to the expression. And the hiding operator has an argument, which is a set of actions that are actually hidden. So besides the hiding operator, which hides the actions that I mentioned in the set i, we have a renaming operator and a renaming operator has a renaming scheme as an argument. For instance, you can have this renaming scheme where you rename a in b and c in d, and it simply renames the action according to the scheme. There's also the blocking operator and the blocking operator renames the actions in this set which, into delta, and historically the blocking operator was called encapsulation operator so we use both names. These are really just renaming operators. A hide operator renames to Tau, the blocking operator renames to delta, and the renaming operator renames one action into another action. So that means that they have also, similar actions, and I am only giving them for the hiding operator. So if I hide something into the internal action, everything is already hidden and nothing needs to be done. If I have an action, and here I put the data parameter d to the action to indicate that it can also be applied actions with data, and it can be zero or any other number of data parameters. And we rename this action with data to Tau if the action label occurs in i, and if this action label does not occur in i, we leave the action untouched. For all the renamed operators it holds that they distribute over multi actions, that delta is not changed under renaming. It's obvious because there are no actions in Delta. That we distribute the operators of the choice operator of the sequential composition, and of the sum operator. Now that we are discussing axioms for internal actions, anyhow, it's probably also time to mention the axioms that belong to branching bisimulation and weak trace equivalents. So let's first look at rooted branching bisimulation. The first action is, and the most important action, that if you do with Tau, often if you do a process followed by an internal action, then you can remove that internal action. Typically if we have a process A tau B, say, then the tau is preceded by the A, therefore I can simply remove it like this. There another action, namely this one, and it can be shown that in the context of pair emulation this action is really needed. And this is really considered the branching bisimulation axiom and it more or less expresses that if you have information that becomes slowly available then you can also consider it as being immediately available. So if I have a process X, the after that Y becomes already visible but I have to do some internal step tau before I also can see the behavior of Z besides Y, then this tau can be omitted then we can also immediately see Y plus Z after the X So in the picture, if you have this a followed by b or after tau b and c become visible, then that's actually equal to this process, a immediately followed by b and c. So we can also ask ourselves, what are the axioms for? Weak trace equivalents, well the same axiom where you can remove a tau after a process with and only with trace equivalents you can also remove a tau before a process. So if we had this process tau for a b, we can actually remove the tau and b is the result. And using these two axioms almost every tau in a process can be removed. Okay let's do some exercises. If you have this process expression, where you have tau a, applied to the communication of b c, goes to e, of a b in parallel with c d, what is then the true statement about this process? Second exercise, here we see two identities, we actually have quite a lot of identities but here we have two. Are they valid? We have to have introduced the hiding and blocking and renaming operators. We showed what the equations were there for these operators, and we also introduce the axioms for rooted branching bisimulation and weak trace equivalence. In the next lecture I will try to analyze a well known mutual exclusion protocol, namely Peterson's algorithm. [MUSIC]
