[MUSIC] Nice to see you again. In this lecture, we will speak about abstraction techniques for data to keep the state space small. So when you want to reduce the size of your state space, be very aware of data and try to reduce the use of data whenever possible. So one way of doing that is that you can limit the number of values in your model. So instead of using a distance, you could probably replace such a whole domain by a few values, for instance, near, far, or very far, or something like that, or, even, just one single distance used, a constant distance. You could also consider reducing the input to only a very small number of cases. You may find that that's not really desired because you would like to know that your system works well under all circumstances. But, what one then sees, is that one cannot prove the correctness of the system anymore and one has to establish the correctness by, for instance, testing and by just verifying the equipment for a few input values. You find many more problems and uncover far more books then by just testing. So, it's far more effective to check the system for just a restricted number of input values, if you can not check them for all. Actually, it is the case that if you have a realistic system, then the number of dates are often so big that it is extremely time consuming to do a verification. And a very good strategy is to actually restrict all your data domains to trivial data domains, then do a first round of verification, if that succeeds, slowly increase the size of your data domains. If you have to wait for verification for more than a few minutes, then your data domains are generally too big. So let's look at a concrete example. Here we have a car that approaches a movable barrier, and there is a distance detector with an associated controller, and the distance detector measures the distance to the car, and if the car will pass the movable barrier during the next measurement, then it will quickly open the barrier, and we assume that opening the barrier does not really take time. This is the controller, it has two actions. It measures the distance with an action distance, d, and it triggers the barrier to open with the action trick. The maximal distance, that can be measured as m, m as in it's file number, and we take m to be 100, in this particular case. And behavior of the whole system is described by this line, where you can see this process distance controller. And it recalls the previous distance that was measured. Initially, this previous distance is set to the value, m, that's the maximal measurable distance. What we see is that the controller measures a distance. And if the distance is smaller, of if two times the distance is smaller than the previous measured distance, then the car will pass the barrier before the next measurement, so the trigger action should be sent. And if the distance, two times the distance is larger or equal than the previous distance, the car will not pass the barrier and the just measured distance will actually store it into the previous distance and the process will repeat itself again. What we see is that the state space is actually 10,000 states big, and this is quite amazing for such a simple system. And the reason for that is, that at this particular spot, not only does the distance, d, but also the previous distance must be recalled. And what we also see is that the only information from the distance and the previous distance that is actually being used is this condition. So its only a Boolean information, namely that 2d is smaller than the previous d or not. And we can use this by moving the condition to a slightly different place and this will already have an enormous effect on the state space. So this is the new inscription, and what we have done is that we moved the condition before the action dist. So this first action dist, now represents measuring the distance when 2d is smaller than d pref, and then a trigger must be sent. The second action dist means that we measure the distance, while the car will not pass the barriers during the next measurement. And then, we just give this just measured distance, d, as an argument to the distance control to be recalled for the next round. What we see is that we only need to record the value d here. And that has an effect that the state space of this whole system is only handled in one states big, and that is substantially smaller than the 10,000 of the previous state space by just moving a condition. But you can even do better by not measuring concrete distances, but by just abstractly measuring whether the car is even near to the barrier or far from the barrier. So we replace the data domain barrier to abstract data domain, two failures. So we have now the abstract distance controller and it reads the distance, if the distance is near, it sends the trigger, otherwise it simply repeats itself and the initial state is just ADC without a parameter, because that is not needed anymore and what we see is that the whole state space is only two states big. So here, we have an exercise and what's very useful is that one can measure upper bounds on the states space by looking at the size of the data domains in the linear process. So, the question here is, if this is our linear process with four parameters and that domain, D1, has 7 elements, D2 and D3 have both 10 elements, and D4 has 2 elements, what is then an upper bond on the size of the state space? So, what did we do? We looked at data and we should be very careful with data as otherwise, we'll get a state space explosion. So, if possible, our data domains should be made as small as possible, or even better, one should replace the data domains by abstract data domains with abstract values, if that leads to smaller domains. One can increase the size of the model by storing data at places where one may not be aware of that. So sometimes it may help to investigate the model for these stored places of data and reduce the size by, for instance, moving conditions to another place. If the state space is still too big, once you've seriously considered to verify the system under very strict scenarios where the environment can only offer a limited amount of values, and the reason for this is that it is far more effective to analyze a system using model checking under all kinds of scenarios, than when one uses the alternative, namely testing, because that leads only to detection of the obvious problems in your system. And the last thing is that once you start by extremely reducing the data in the model, when one starts verifying the reason for this is that if you can't verify your system under usual circumstances, you'll certainly not be able to do it, then the data domains become larger. And if you find yourself waiting for the response of the tools to do a verification for more than a few minutes, and you have no idea how long it will take, then probably, you should first consider reducing your data domain. In the next lecture, I will address sequentializing the behavior of parallel components, to reduce the size for the state space. Thank you for watching. [MUSIC]