[MUSIC] Welcome again. In this lecture we will deal with one of the most important notions, namely notions of bisimulation, and we will give its official definition. So assume we have a transition system given, then we say that a particular relation R that relates A states is a bisimulation relation if and only if it relates two states, like this, s and t, and we can do an a step from s. Then, it should be possible to mimic that from t, like this. You can have more choices, but the choice you select at the right hand side should be such that the endpoints are again related by R. In the definition, it's like this. If s can do a step to s prime, for some state s prime, then their should be a state t prime, such as there is also a transition from t to t prime, such that s prime and t prime are again related by R. The definition of bisimulation also allows It to check from the other side of our, it obliges you to check the other side. So if you can do the step from t, so we have two states that are related. We can do step from t. Then it should be possible to mimic that by s, from s, such that the end points are again related, and in a formal definition this looks like this. So if you can do it a step from t to t prime, then you should be able to mimic that by doing an a step from s to s prime, such that s prime and t prime are again related. We also have to deal with termination. So suppose we have two states, s and t, that are related. If one can terminate, indicated by this tick symbol, then the other side should also terminate. And if you have the same, but one side can not terminate, then the other side should also not be able to terminate. And this is expressed by the following, namely if s is an element of the terminating states, then and only then, t should also be a member of the terminating states. Now when are two states bisimilar? Well, if we have two states S and T and we can find a bisimulation relation R that relates them, then we say that these two states are bisimilar and we use this typical notation for that with a double arrow that is underlined. And if they have two transition systems, we say that the two transition systems are related if the initial states are related. Okay, let's see whether we can apply this to some examples. So, consider these two transition systems, and we want to prove them bisimilar. So what we have to show is that there is a bisimulation relation that relates the initial stage. So assume such an arbitrary relation. We relate the initial states. And then we will try is we will extend this transition relation over all transitions of overall states and see where it satisfies the properties of bisimulation. So, if we have an a step at the left, then it should be possible to do an a step at the right, and the end point should be related as indicated here. And now, suppose that the states in the middle are related. If we have a b step at the right side, then it should be possible to limit that at left side, so it should also be the case that these two states are related. And similarly, if we look at the states in the middle and if we do the c step at the left, then it should be possible to maybe get by c step and so, this can force these two stages to be related. And what we can see is that for all paths of states, the properties of the definition of bisimulations are satisfied and this means that we now find a proper bisimulation relating the initial states. And so, we can say that the initial states are related. So here we have another example. You probably recognize this example. This is the example of the princess and the dragon so they should not be related but how can we find that out? Well, we do that, as follows. We relate the initial states. Again, any attempts to show that this relation r is actually bimulation relation. And we will ultimately figure out that that cannot be the case. So what's extremely useful is that you look at the non-deterministic sides at the left site, and you do an a step or assume that we do an a step to the state with the outgoing b. And then, we can try to mimic that with the a step at the right. And that means that if the initial states are related, then, these two states should also be related. And now, you can now see is that if these two states are related then we can actually do a c state at the right, but we cannot mimic that at the state at the left. So these two states cannot be related, but we have to relate these states if the initial two states were related. So that means that also the initial state cannot be related. And this means that there cannot be a bisimulation relation that relates to initial states, and that means the initial states are not bisimilar. There's a very nice property of bisimulation equivalence and that is the following. Namely, every transition system that you have has a unique minimal transition system, that belongs to it. And the use of it is the following. If you have a big transition system, we calculate as minimal transition system and then we store the behavior in this minimal object. So let's look at an example. Here we have a transition system that can do five a's and then repeats itself again. And what you can imagine, is this transition system can do typical human behavior of doing an infinite number of a's. Well, there is a much simpler transition system, namely this one, that can also do an infinite number of a's. And this is actually the unique, minimal transition system that is bisimilar to the transition system at the left. How can we prove that? Well very straightforwardly, we have to find a bisimulation relation that relates the states from the transition system at the left with the state of the transition system on the right. And we should show that they satisfy the properties of a bisimulation relation. And this is actually the relations over here. We relate all the states at left with the state at the right. Okay, let's see whether you can do this yourself. Let's look at this two transition systems and the question to you is, can you prove or disprove that these two transition systems are bisimilar? A second exercise. Here we have these two transition systems. They are obviously not exactly equal. But are they actually bisimilar? And a final exercise. So, we call this alarm clock. We have this behavior of the alarm clock where the alarm could sound only once. Here we have the behavior of the alarm clock where the alarm can sound infinitely often. And the question is: are these two bisimilar or, more precisely, is the left state off similar to the right state off? The left state on bisimilar to the right state on? And are they initial states? Or are the alarm clocks bisimilar? Okay, what have we done? We have defined precisely bisimulation or strong bisimulation, both names are being used. And we have shown how you can for simple examples prove or disprove that these transition systems are actually bisimilar. Thank you for watching. Next lecture, we'll deal with trace equivalents. [MUSIC]