[MUSIC] Nice to see you again. This time I want to extend the modal formulas with data, and this will provide you with the most powerful modal logics currently available. We can add data to our modal formulas. Let's start with actions. So, what we can do is we can add, just as in processes, parameters to the actions. And then we can write down diamond (a[1]) phi, which represents we can do an a1 action after which phi holds. We can even use variables or expressions as parameters of actions in these modal formulas. So, we can typically write down there exists an x of type natural number such that we can do an a[x] action phi, and typically we can use this x inside phi. We can also use the universal quantifier. So this expresses that for all natural numbers x, we can do an a[x] action after which phi holds. So, a slightly more concrete example is this one, but now with the box modality. And this says, for every natural number x, if we perform an a[x], then x must be larger than 3. So this says we can only do a[x] actions with the property that x is 4 or larger. So, let's immediately apply this to an example. And a nice example is the unique number generator decision device that generates numbers which generate action. And the property of these numbers is that it can never generate a number twice. So all the numbers should be unique. And how can we actually express that? Well, it's very straightforward. Whenever it generates two numbers, so a number x, and a number y, they should be different. So, we first do a sequence of actions that could be generate actions in between. If you then do a generate(x), and then we do an arbitrary number of actions, again, with potential generate actions in between, and we do a generate(y), then x should be different from y. And students saw this when I wrote this down on the blackboard and they said, well, you can even do this more compactly. And that's, of course, the case. So, this is an even more compact formulation of the same formula. Namely, whenever I generate the value x twice, that is not allowed. So then we end up in a state that cannot exist. And this is typically stated with the box modality and false at the end We can also add variables to the fixed point operator. So, suppose we have this process that represents a Room, and we have an in action and an out action. In means somebody enters the room, out means somebody leaves the room. And the property that we want is that nobody, that the number of people leaving the room does not exceed the number of people entering the room. If that would be the case, all things would happen inside the room. And how can we express that? Well, we do this by adding a parameter to the fixed point variable. So what we say is that we have a maximal fixed point operator of x. X has the parameter n, and n represents the number of people in Room. And initially, n = 0, so initially we assume there's nobody in the room. And we say that whenever the in action happens, so whenever somebody enters, we go on checking this formula but now with the number n+1, indicating that there's one more person in Room. We can also do the out action, and that means somebody is leaving. So whenever somebody is leaving, we check that n is larger than 0. If that is not the case, Then there are more people that left the room than entered the room. And the formula after the box modality becomes false, and because we used ands on the right hand side, the whole formula becomes false. And we can see that a property that's the number of people leaving the room is smaller or equal than the number entering the room, is invalid. The second part after the box modality says x(n-1). And it says that we continue checking this property, but now with (n-1) persons in the room. It can also be that there are other actions than in and out. And if these happen, we should not change this value n. So what this says is we have the box modality of in and out, so in for united with out, but then it's the complement operator. And this says that whenever we do something else than in and out, we simply continue checking where we keep the value n unchanged. We can type these formulas into the tools with the obvious changes, so the and should as two &&, and the complement is actually written down as an !, and the union as a +. But there are two things which can cause confusion if you would do this. The first one is that if you use an expression, you should use vowel in front of that expression, because the posture will not always properly recognize what's an expression and what's a modal operator. And this has been resolved by the introduction of this somewhat unfortunate vowel. But this is what the partial requires around every expression you should write for. There's another point, namely, we write down (n-1) here. N is a natural number. If you write down (n-1), this becomes an integer, and you have to add this typical typecast to guarantee that (n-1) is again a natural number. But, except for such changes, the tools accept these modal formulas, including quantification. Another example, this was an example that took us quite a long time to solve. And the reason was that we tried to solve this without the use of parameters in the modal formulas. With the use of parameters, it's completely straightforward. So, what's the idea? We have this merge process. It has two inputs, in1 and in2. And there's a stream of numbers being read at in1, and there's a stream of numbers being read at in2, and there's a stream of numbers delivered at out. And the property that we want to check is that as long as the stream of numbers at the input is increasing, the output should be increasing. And we're not really interested in whether the numbers are the same, so our property will not deal with that aspect. It's just about the effect that the sequences are increasing. And you should note that we are writing down an observer with our modal formula. So, somebody implemented this merge process, and our modal formula checks whether it actually is correct, in the aspect that when inputs are ascending, the outputs is ascending. So how do we formulate this? We take a maximum fixed point operator. We put two parameters in there, n 1, n2 and m. And so the meaning of n1 is that it is the last value read at the in1 gate. And n2 represents that last value read at in2, and m is the last value that we delivered. So we can write the modal formula as follows. Whenever we reach a value at in1, so for every natural number x, if we perform an n1x action, then, if x is smaller than n1, the input is not ascending anymore and we can stop checking, the right-hand side becomes true. And this point of the formula becomes true, so it stops checking at this point. Or if the input is ascending, then we have to check this other part that we find after the box modality. And this asks that we have to check the formula where we replace n1 by x. Namely, x is the last value that we read at in1, and we simply have to continue checking. The same holds for reading the number at in2. So, if we read the number at in2 and it is not ascending, we can stop checking, but if it is ascending, we have to continue checking with x at the place of n2. And whenever our system, so we call the modal formula, monitors the behavior, so whenever we deliver a value at m of at out, then the last value we delivered was m, then it's okay if x is increasing. So, if x is not increasing, the formula becomes false here. And due to all the conjunction, the whole formula will become false. But if it's okay, we have to continue checking, after delivering this value, that the behavior is also okay for all the other actions to happen. So, this formula expresses that as long as the inputs are increasing, the output sequence is increasing. It could be the case that we have more actions than in1, in2 and out. And if that is the case, we add this line. And this line says that whenever we do another action than in1, in2, and out, we simply continue checking without changing the parameters of the formula. And you can see something special here, we can use the x's quantify insight modal operators also, and that is what we use in this particular case. So let's go to a number of exercises. Here we have a formula where we use data, and the question is, what does it express? And here we have a second exercise. Do you have any idea what this formula means? So we've seen that we can use data in actions in modal formulas. We can even use arbitrary expressions of data in these modal formulas. And we can use quantification as well. Using parameters, or fixed point operators, we can express quite complex properties. And actually, what's the case, is that we have the most expressive modal logics currently available here. So some people may like LTL and CTL, linear time logic and computational tree logic, but the language here is not only far more expressive than these logics for the properties expressable by these logics, this language is equally powerful as well. In the next lecture, I will show you minimal and maximal fixed points used alternatingly. And using that, we can also express fairness properties. Thank you for watching. [MUSIC]
