[MUSIC] In this lecture we will look at simple data transfer protocol, namely, the alternating bit protocol, and we will see how we can use branching bisimulation to show that it actually behaves as intended. In the alternating bit protocol, we want to send data from left to right, as in this picture. But the data must be sent via an unreliable medium, something where messages can be lost. And the idea is that we add an extra bit, the so-called alternating bit, to this protocol. And they care by this bit the data transfer goes in the correct way. So data can be sent from one side to the other and it can be that it arrives correctly. Or data can be sent and then it's lost, and so the data will never arrive at right-hand side. Fortunately, it is possible to send data back and forth and this allows us to send acknowledgment saying that certain data did arrive and other data did not arrive. So we have one channel, we call it K, and that is being used to send data from left to right in this model's unreliable data transfer. So in alternating bit protocol, we will send a message and a bit to the other side. In the channel L, we will send acknowledgments back, and it suffices to only use a single bit, so a single value true or false, and sends that back. So that's being sent back. And so the behavior of this channel L can be modeled as follows. So we have the initial state, and in initial state we will receive at channel r5 either true or false. And if it has arrived in the channel, then the channel can decide to actually forward it. This is some internal process. Or it can decide to lose the message. So this may also be determined by whatever happens inside this channel. If it is forwarded, the data is delivered at gate s6 and acknowledgments arrive intact. And if it is lost, simply a lost message is being sent to the left side to indicate that data transfer was not going well. The same holds at the right-hand side. So if we receive a false message then the data can get lost or it is transferred to the other side, so forwarded correctly. And if it's forwarded correctly, the false is delivered properly to the left-hand side. So what we want to see now is how we can analyze this behavior, and we do this by actually putting two protocol entities there, so the behavior of protocol R and protocol S, that add these extra bits and checks that the right bit is being sent to the other side. And what we want is we hide the internal communication and we only want to look at behavior at r1 and r4, because there we expect that the data is reliable, so every data is sent to the other side exactly once. So there is some communication between the different components. We hide this communication and we only look at the external behavior. So let's now look at how we can analyze this behavior and use the tools for this. And we look at the folder. It's the alternating bit protocol, which we find here. And in this file, abp.aut, aut for automaton, we find the transition system of the alternating bit protocol. And this is how it looks like. So there are different formats for transition systems. And the AUT format has yet found that it's quite readable, so it looks like this. You have a descriptor saying that the initial state is state 0. There are 92 transitions, 74 states, and the transitions are all listed here. So from state 0 to state 1, you can do a r1(d1) action. And from state 0 to state 2, you can do a r1(d2) action. You can see of the majority of the transitions are tau transitions or hidden transitions. Which can also go with the s4(d1) action from state 10 to 14 meaning that you deliver datum 1. And this is a relatively small transition system, so you can see the number of states is not that big at all. If we right-click on the name of a file, then we see what we can do with the file. So there are several tools for analysis, and our transformation tools that work on a file of type AUT. And one very useful tool is the LTS graph tool that visualizes the transition system. So if you click on that you'll get a window here with all possible options that are available. Here below there will be a statement that you can type in. For instance, for the use of scripts to run all these operations automatically from the command prompt. And if we press Run the tool will actually be started. So here we see the tool and we see the individual states. This state is the initial state, and if I right-click on it, then what we see then the state clicks through the canvas. I can move the states around but a very useful feature is to actually automatically let it optimize. So if I take the length of the individual transitions to be somewhat shorter. If I click this state to it confirms below, and I help its transition system a little bit to get into shape, then what I can see here is a read 1 d1 action. What I can see here is a read 1 d2 action. And I can see the behavior becomes somewhat decent. So what you see here is that data is being read, so d1 or d2. Then this cluster here indicates that the data is lost while transferring it from left to right in channel K. If that is successful, then actually it's delivered. Here you see this cluster here indicating that acknowledgment is lost and that retransmission takes place. But if retransmission is successful we get to this state, where the bit of the alternating bit protocol is changed from 0 to 1 or from true to false. And then we see exactly symmetric behavior here. Data is lost while sending it to the other side. Data is lost in sending the acknowledgment. Here d1 is read, d1 is delivered. A nice feature is that you can also look at this behavior in three dimensions. So that's being done by choosing the 3D option and because this has these four legs you can see that structure. You can visualize the behavior of this system quite neatly. This frame depends on the structure of the database and the number of states that you have. Often I prefer to use this 2D view. One of the big disadvantages of this system is that the number of states are often quite big, so we would like to reduce this behavior a little bit further. So let's do that. So we choose the file again, we can take the LTS convert to, and what we see here now are all kinds of reductions. We are especially interested in branching bisimulation so let's select that and let's do the reduction. But let's give the new file a new name, so I'll call it abpreduced.aut. And I can run it. And then here the new file appears and I can visualize it using LTS graph again. What I get is this state space and if I let it shape itself automatically and I increase the transition length a little bit, this is the actual behavior after reduction mode low branch bisimulation. And what you see that the initial state is here. You can read a d1 action which is here. And a read d2 action after reading the d1. Sorry, the d1 is being read there. After reading the d1 it's delivered once and only once exactly, as we want to have that. And only after that we can read the next datum if d2 is read, d2 is delivered. And from this picture we can see that the behavior of the alternating bit protocol is exactly what we want it to be. What is interesting is to make small changes in the protocol. So these protocols are very tedious and hard to make correct, but it's very easy to make them incorrect. So let's look again to this behavior of the channel L, and let's change the behavior a little bit. So let's assume that we do not want to send the lost message explicitly to the left-hand side. So we remove that lost message. We remove the loose message but we move it directly to this initial state. And we'd also do that with the other side, so we remove this loose message and move it to this state. Now what you will find on the Coursera website is a file with a transition system. And the question is, what happens if you actually reduce this behavior and then visualize it? How does it look like and how can you see that the behavior is not what you would like to have? So what did we see? We saw the sketch of the behavior of the alternating bit protocol. We showed you what behavior was and then you use that branching bisimulation using the Itsconvert tool. And we visualize the behavior before and after behavioral reduction using the Itsgraph tool. And we could see how the behavior was indeed correct using these tools. Thank you for watching this video. In the next lecture we will speak about divergence preserving branching bisimulation as a slight adaption of branching bisimulation. [MUSIC]
