[MUSIC] Nice to see you again. In this lecture, I want to introduce the notion of a linear process. If you look the structure of the toolsets, then we can see that we have all kinds of formats that we use. And all kinds of transformations. So here, are mCLR2 specifications. But which we start, and then we always transform them to so-called linear processes. And that is this form up here. And what we have already seen a number of times, is that linear processes are transformed. To label transition systems, that we can then reduce and inspect. But in this lecture I would like to speak about how linear processes look like. And they are really helpful if systems become very complex. So what's a linear process? A linear process is a Indicated by this somewhat, well, horrific expression. But as you will see, this looks worse than it actually is. So what's this important un-ilinear process? We have one variable which can have any name, but I prefer to use X. And this name occurs also on the right hand side. On any place on the right hand side, we use the same process variable, as at the left hand side. And that is, what this has said. Furthermore, we have a number of parameters of this process faramo. If I write down a linear process, in abstract way, I always use one variable that is convenient. But that can actually zero or more variables, and if you look at it formally, then using stricter data types, you can always transform zero or more variables into one. So formally we can speak about one single variable, if it comes to applications and examples, I use an arbitrary number of these variables, if it comes to this general format or to tiery, I always use one single variable. Here, we have this sigma, with the subscript I is element of I, and that indicates that we have a finite number of sums. So, this capital I is an index set, which must be finite. And everything that follows the sigma is called the summand. A typical example is the following, where I left out all data. So if I have a process, with condition cvon and if cvon holds I can do an A1 and end open X again, or I have a second summand, C2, with conditions C2 and action A2. And even a third one. Then I can write this concisely, using this sigma or symb, with an index as a subscript in this way. So then the index contains three elements, 1, 2, and 3, and the i occurs at the positions of the 1, the 2, and 3 in the individual summands. And this allows me to write down a linear process in a single line. If it comes to examples, I generally prefer to write down the individual summands. So, let's inspect this linear process further. Here, we have conditions. And the conditions depends on the parameters of the process, and this ei I will address later. If the condition holds, then we have an action. An action can have zero or more parameters, and that's indicative if the function, f i, dependent on d and e. And what is important is that we have only one single action, at this particular spot. It's not allowed to have more than one action, and that is the most important feature of a linear process. And after performing this action, we end up in a process X again. We end up in this process X, and the effect of the action is encoded by this function g i, in the parameter, of the process. In each summands, we can also use the sum operator, where we take a variable e i of sort E i. And this indicates that we can, freely choose values for E i in the right hand side. So let's look at a small example. Here we have the process P, is a, b, P, and this is not a linear process, because we have two actions in front of the P. And that is actually not allowed in linear process. And the question is, how can we transform this particular process, to alien a process. And the idea is to introduce a boolean, C. And if C is equal to true, then this indicates the state directly before the A, and observe that the states directly before the P is actually the state directly before the A. So these 2 spots are indicated, with c becoming true. And see if c is false, then this indicates we are between the a and the b. So what we can do now, is we introduce a process with the parameter c. If c is equal to true, then we can perform the a action. And we end up in the state characterized by C is equal to false, so after the A we enter an X false. Or, if c is equal to false, then we can do the b action, and we end up in a state, correct, right, where c is equal to true. And this is the linear process, belonging to the process equation of. And you can see here, that linear processes are, in general slightly unreadable for humans, but for the tools and for the theory, they are extremely convenient. So an important theorem is that almost all processes can be linearized to this format. Actually there is an issue with terminating processes. If we have terminating processes, we have to extend the format of linear processes a little bit. But for practical purpose,s it is sufficient to recall that each process can be linearized. Including processes with parallel behavior, with the communication operator, with allow, hide, etc. These simply are removed in the process of linearisation. Unfortunately the tools that we have cannot linearize all the processes, only parallel pCRL processes and what cannot be linearized is when we have recourse in the scope of, for instance a parallel operator or the communication operator or the allow operator. That does not work. Although that's theoretically possible, but it has not been implemented. What we see, is that all practical examples that we will encounter, can be linearized. So, an example of a process that cannot be linearized, if we write down, X is a ,X parallel b, you see that X occurs in the scope of the parallel operator. And therefore the linearization will refuse to linearize this, and if you put a recursive X in the scope of the allow operator, then that will actually also not be linearized by,with the tools. So let's take a slightly more complex example, the buffer. This is the equation that characterizes the behavior of the buffer. We read an element d of tag d, we deliver that element, and then buffer repeats itself. So, if you want to linearized this, we can introduce this boolien as in the previous example. But, and what we can see, is that this state in the process is characterized by C is true. And it also holds for directly before B, we can also see that we can define that the middle part, its categorized by setting C to false. And if you look between the read and the deliver, then we can see that at that spot we have to recall the failure of d, that we just read to be delivered. So, we need another variable which we call d prime. That recalls this intermediate value, so our linearized process has two parameters, and looks like this. So, we have the parameter c of type boolean, d prime of type d, and if c holds, then we can actually read a new d. And here you see the sum operator occurring in the summand in the linear process. And it will set the value of d prime, in X to d. And it will also set c to false, indicating that the next action is to deliver this data. And if c is false, it actually delivers d prime. And it moves back to X where c is set to true, indicating that the buffer is now ready to read a new value again. What we can do is just have a short look, on how the tools linearize this buffer. Here we have the buffer. Let's look into it. You specify the buffer with this equation. Initial state is B, and we took the domain d to have two elements such that I can also show the similitude to you. If you want to linearise this, use this mcrl22lps. We run that and we get this linearise process. And we can make this human readable, by using the LPS predy print by LPSPP. Which actually generates a file buffer dot text. And this is our linear process. So what we can see is that the data are the same, the accents are the same. We have this process here, now the state is not a boolean, but a positive number, and if the number is 1, we can do the read action. If this number is 2 we can do the deliver action, initial state is 1. We see that the D prime from the slides, actually has the name DB as B refers to the name buffer, so that you can recognize different parallel components. And we can see that we have these glob variables. These are variables that can take any value, but the result is still strongly by similar to the original. And this allows the different transformation tools, to select optimal values for certain parameters in this particular process. What we can do is, we can simulate a linear process, so we use the tool lpsxm for that. It's below here, we can see here the actions we can do in the initial state, we can read D1, we can read D2. So select with D1, then we see here the trace that we can do, after reading D1, we can deliver D1 then we can read D2. And what we can see below here, are the values of the parameters in each state. So, after reading D2, we see that the value of DB becomes D2. And the transformation to linear process is sometimes smart. So, there's not always a one to one correspondence to where you expect. But, by and large, you can see the values of the parameters, of your process, fairly well here while simulating. Here we have an exercise, we have two process equations. Are these process equations actually linear? And here is the second exercise, if you have a process with three actions, how can we linearize this? And I have four suggestions here. And there's only one that is correct. So what have we done? We introduced the notion of linear processes. We saw that all processes can be linearized, except for those processes with termination. But that's not really so important that I want to spend a lot of attention on that here. We saw that we have this tool, mcrl22lps to linear processes, and it can linearize all practical processes that we will encounter, but not all processes that you can write down. And it is important to realize that linear processes are not always convenient for humans. But they are extremely convenient for the tools. And also extremely convenient, if you want to develop more theory about processes. In the next lecture I will show how we can manipulate linear processes. Thank you for watching. [MUSIC]