Actions, multi-actions, alternative and sequential composition
System Validation (2): Model process behaviour
EIT 디지털
System Validation is the field that studies the fundamentals of system communication and information processing. It is the next logical step in computer science and improving software development in general. It allows automated analysis based on behavioural models of a system to see if a system works correctly. We want to guarantee that the systems does exactly what it is supposed to do. The techniques put forward in system validation allow to prove the absence of errors. It allows to design embedded system behaviour that is structurally sound and as a side effect enforces you to make the behaviour simple and insightful. This means that the systems are not only behaving correctly, but are also much easier to maintain and adapt. 'Model process behaviour' is the follow up MOOC to 'Automata and behavioural equivalences'. This MOOC shows you how to model process behaviour, in particular protocols and distributed algorithms, dive deeper in the properties of system behaviour, and keep things simple to avoid a state space explosion. Reading material. J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT Press, 2014. This course is part 2 of the set of courses for System Validation. System Validation, as a set of courses, is part of a larger EIT Digital online programme called 'Internet of Things through Embedded Systems'.
Sequential behaviour
Introduction MOOC model process behaviour2:45
Actions, multi-actions, alternative and sequential composition9:26
Process axioms11:01
Jan Friso Groote
[MUSIC] Welcome again, in this lecture I will show you the basic process operators to specify elementary process behavior. We saw that behavior was built out of actions, so it's a simple light example, you have the switch on action and the switch off action like this. And in this way we will also build our process language, so we start with actions. Generally called a, b, c, and d if we speak about abstract actions and then we speak about concrete actions. We give them nicer names, and what we assume about these actions is that these actions are atomic. So that means they do not have any duration at all, they are just happening in an instant in time. And now you may say that you don't like this because you have actions that take time. Well, actions with a long duration can be modeled by simply indicating when it starts within an atomic action and when it ends. There has been a long debate on how we should model actions and some people say that it's not correct to model on the basis of atomic actions. These people speak about true concurrency. Others say, well we simply use atomic actions and these people more or less adhere to what's called false concurrency. If you have a action look like as a transition system, well, it's simply this transition systems. So we have an initial state, the a action can happen, and after the a action happens, we end up in a state where we can terminate. And that is the state where subsequent actions can actually happen. So, if you have actions, we can add operators and one major operator it is sequential composition operator, it's simply expresses that first p happens and then q happens. And we write it down as and quite often we have tendency to even leave the delta out. So suppose we have this process that doesn't A, and then B how does it look like? Well, the behavior from the a is this mainly we a and then terminate. The behavior is the b, it's almost equal. We can do the b and then terminate and if we combine them, what happens is the first do of a, a two minutes the behavior move towards going to b and at the end it will be next. So, the intermediate termination has disappeared another important operator is the alternative composition operator written like p+q. And it says that you can either do the behavior of p or the behavior of q. So, as an example, consider a+b, here we have a again, here we have the behavior of b and the behavior of a+b is constructed as follows by just merging the initial states of the two processes. And you can see that after doing the a and after doing the b the process can still terminate with these operators we can make more complex behavior, so consider a.b+c.d. First, do an a, followed by a b, or a c, followed by a d and you can imagine that this is the behavior that belongs to it. If you look at the last state We can see that this behavior is the same and that these dates are bisimilar and we can merge them. And that is what we sometimes do and then we get this behavior and then we can put an e after this behavior. So, we get the behavior ab or cd, both followed by e and typically this is the behavior that belongs to it. Of course we have to remove this intermediate termination symbol. There's one typical constant in our process algebra which is called deadlock or inaction, and it is written as a delta. And it stands for the process that does not do anything at all. In particular, it does not terminate, so this is the transition system that belongs to it. And then we can have the behavior of a followed by delta, and that is bf of a and what the delta dash is, that's it. Says that if you can't go on after doing the a, so it simply remove this termination at the end of the a. You can also look at the behavior of delta followed by a, but because delta can never terminate this behavior will never be able to do the a. So the behavior, the system belonging to delta followed by a is simply the same as behavior belonging to that log itself. Sometimes we have systems were actions can happen at the same time and these are called multi-actions. So if a and b happen at exactly the same instant in time, we write this as a bar b. And we can also let three actions happen at the same time so write it as a bar b, bar c. So there's a multi-action with three elements, it can even have more of the same actions in a multi-action. So suppose we have this behavior with two actions, a and these actions a can happen simultaneously so a | a is the action where you have two actions, a, happening. The multi-action where you have two a actions happening simultaneously and you can also have five a actions happen simultaneously as written here. A typical of the empty multi-action where an action is happening, but you do not observe anything. Is simply the tow as we have seen before the hidden action an important property of multi-action data or doing multi-actions does not play a role. So, if you have the multi-action a, b, or a and b happens simultaneously you can write it as a b or b a but it is exactly the same multi-action. What's the label for tissue system belonging to a multi-action? Well it's quite simple, instead of the action, we simply write the multi-action. And, we can combine behavior, in the same way as before. So, if you first do a and b simultaneously followed by a c, then this is the behavior that belongs to it. So lets look at a number of questions. If you have the expression a + b followed by c followed by the multi-action d e, what's then the behavior belonging to this process expression? A second exercise, you probably still recall the definition of strong bisimulation. And instruct or specifying the behavior by explicit transition system we now specify the behavior by process expressions. And the question is which of these pairs of process expressions actually express by similar behavior, we can have process expressions in which we have deltas and taus. If you have the process expression a followed by c, or b followed by delta, followed by tau e, which of these four transition systems is a transition system? Belonging to this expression. So, we looked at the elementary process operators, they are built up from atomic actions, we have multi-actions. The empty multi-action is actually written as the taw which you have also seen the hidden action. Sequential composition allows us to say that some behavior should happen before other behavior. Alternative composition allows us to say that you can choose among different behaviors and we have the deadlock or the inaction. That is a behavior that cannot do anything at all. Thank you for watching, in the next lecture I will show you the basic axioms for process behavior. [MUSIC]