0:00

[MUSIC]

Â Welcome at this lecture, where I will explain to you what regular formulas are,

Â and regular formulas are very convenient to express all kinds of properties.

Â We introduce action formulas to represent sets of multi-actions,

Â and they can be used inside these modal operator shell.

Â In particular, they can be used to in a diamond modality and

Â they can be used in the box modality.

Â The syntax of this action formula is the following.

Â Mainly, we can have a multi-action, so from this point on,

Â we can actually put multi-actions inside the modalities.

Â We have this true, and that represents the sets of all conceivable actions.

Â We have false, that's the set without any actions, or the empty set of actions.

Â And actually, I do not quite like this set.

Â True and false, it's there for historic reasons, people started to use it.

Â But representing these sets by true and false is confusing,

Â because true and false are used for formulas and not for sets.

Â Anyhow, we have to live with this.

Â And true means the set of all actions and

Â false means the empty set of actions.

Â If we have a set of actions,

Â then if we write a bar on top of it we mean the complement.

Â So that is the set of actions compliments to the basic sets.

Â 1:37

And in the same way, we can have other sets like operators,

Â like the intersections, so af intersected with af is just the sets of

Â all multi-actions that occurr in both sets.

Â And we have the union, so if we have set one union, set two,

Â then we have all multi-actions occurring in both sets.

Â Okay, so if we have a set of multi-actions a,

Â then what does diamond a phi mean?

Â Well, that's quite straightforward.

Â It means that there is a action a from this set a,

Â such that we can do that action after which phi holds.

Â 2:28

And for the box, we have a similar meaning.

Â So we have again, this set A, capital A.

Â And books capital A phi means that for all actions in this set A,

Â if we performed an action, phi should hold afterwards.

Â 2:51

Now this is what we've already seen.

Â If we say, diamond a phi, this means we can do an a, after which phi holds.

Â And now, we can also write a multi-action b, in the diamond operator phi and

Â this means I can do a multi-action a b after it's phi holds.

Â If I write down true, diamond true phi,

Â then this means that I can do an action from the set of all actions.

Â So an arbitrary action after which phi holds.

Â 3:27

And if I write down false phi, this says, I can take an action from

Â this empty set of actions that I can perform after each phi holds.

Â Now because there is no such action in the empty set of actions,

Â this formula can never be true.

Â So diamond false phi is always equal to false.

Â 3:50

If I write down the complement of a in diamonds

Â modality, then I mean, I can do an action

Â different from a after which phi holds.

Â And if I write down diamond a union b phi,

Â this means I can either do an a or a b after which phi holds.

Â Let's also look at a few examples of the box modality.

Â So box a phi means after doing an a, phi must hold.

Â 4:26

True phi means, true represents an arbitrary action.

Â So after doing an arbitrary action, phi should hold.

Â False phi means, after doing an arbitrary action taken

Â from the empty set, phi should hold.

Â So we do not have to check anything because there are no actions in this

Â empty set.

Â And that means that box false phi is equal to true for any phi.

Â 4:59

If you take the union, the box of the complement of the union of a and

Â b, of phi, then we consider the sets of all of the actions different from a and b.

Â And this says that whenever I do an action different from an a and

Â different from a b, then phi should hold afterwards.

Â 5:35

And we can use the regular formula exactly as the action formula

Â within the modal operators.

Â So diamond r phi, box r phi are typical ways of using these regular formulas.

Â What's the syntax of regular formulas?

Â Well that's this, a regular formula can either be the empty set of traces,

Â not used very often.

Â It can be an action formula, as we have already seen.

Â And you can write down R.R,

Â which is concatenation of the sets of traces of the first R and the second R.

Â And if you write down a +, it's typically the union of the traces of

Â the left-hand side of the + and the right-hand side of the +.

Â 6:22

The most interesting operator I think is this R*.

Â This is called clean star.

Â And it stands for the iteration of the traces represented by R.

Â Namely, you take a trace from R and you consider that 0 or

Â more times and that is typically represented by R*.

Â And there is a small variant of R*, that's R+.

Â And there, you consider the traces one or more times.

Â 6:55

So regular formulas are nothing new.

Â They can actually be completely defined in Hennessy-Milner Logic,

Â and the fix point operators.

Â So if we take this formula,

Â diamond epsilon phi, then this epsilon set

Â represents the empty set of traces.

Â So this says, after not doing a step, phi should hold,

Â which is completely equivalent to say, in the current state, phi holds.

Â So therefore, diamond epsilon phi is equal to phi.

Â If you take the concatenation operator,

Â then that's actually the concatenation of the two diamond operators.

Â You first take a trace from R1 followed by a trace from R2.

Â And that's exactly what the right-hand side expresses.

Â If you take the + operator, this says, we can either take a trace

Â from R1 Or a trace from R2, after which phi holds.

Â 8:15

R star.

Â Most intriguing operator.

Â So R star sets that after zero or

Â more times executing a trace of R.

Â We end up in a state where phi holds.

Â And that is expressed at the right hand side using minimal fixed point in an R.

Â So R phi says that in initial state phi should hold, and

Â then that's okay, you can stop checking.

Â 8:44

Or if phi find does not hold in the initial state, there should be a sequence

Â represented by R, such that we end up in a state where X holds.

Â So from which we can do, this in a finite

Â number of sub strings of R, reach a state where phi holds.

Â And by using the minimal fixed point operator,

Â 9:44

Now we can retrace from R at least once in order to reach a state where phi holds.

Â So we first check, do a diamond R

Â guaranteeing that we have this trace of R amongst.

Â And then we do zero or more times a trace of R and

Â it opens in a state where phi holds.

Â 10:10

So, let's look at a few concrete instances.

Â This formula, diamond <a b="" c=""> true, represents,

Â of course, diamond a followed by diamond b followed by diamond c</a> and

Â that accepted expresses that you can retrace with an a, b and c in it.

Â 10:44

A star true means, that we can do zero or more times a,

Â in order to reach a state where true holds.

Â And if you will look at this, you probably already feel that this formula is

Â equivalent to true because you can always do the empty trace and

Â end up in the current state.

Â And in any state true holds, so

Â 11:24

If you take this formula, true star a true then

Â this says that after an arbitrary sequence of actions, a can be done.

Â So there is a sequence of arbitrary actions followed by an a.

Â So it means that we can end up in a state where

Â a can be done or in other words, the action a is reachable.

Â 11:54

Well, what we did do find that Diamond modality can also be done for

Â the box modality and the situation is completely duo.

Â So box Epsilon Phi= Phi.

Â If we have a concatenation

Â of two modal formulas in a box used to concatenation

Â of the two were box operators.

Â If you have the choice operator, the push of R1 and R2 in the books,

Â then this means that if we perform a sequence of actions from R1,

Â or we perform a trace from R2, phi should hold in both cases.

Â And if you look at American sign, this is particularly expressed.

Â Namely, if you perform a trace from R1 Phi should hold.

Â And if we perform a trace from R2 Phi should hold.

Â And you can see that what wasn't over when we were considering

Â the same situation with the modality becomes an and here.

Â 12:59

If you look at box R star Phi, then this says that

Â after doing zero or more sequences of strings,

Â repeated strings characterized by R,

Â we enter in a state with phi holds.

Â So this means that if we do just the empty sequence, phi should hold or

Â phi should hold immediately in initial state, ends and

Â this is expressed with this boxed R x at the right hand side.

Â If we perform a substring of R,

Â the entrophy in a state where phi should holdt and from which,

Â if we do more of these substrings, we only end up in states where phi holds.

Â So we can see that in all states reachable by sub strings,

Â recognized by R, Phi must hold.

Â And then we have this formula r plus which is exactly the same as with the diamonds.

Â So we express that we should at least do one string from r in order before.

Â 14:55

If I write down true star A false, then you can see that this formula

Â becomes false if we can do A showing here in our system, so

Â this expresses that the action A in not possible in any reachable state.

Â 15:14

And the formula books true star, diamond a through expresses

Â that after any sequence of actions, we can still do a so

Â in every reachable state, an a action can be performed.

Â 15:38

So, it reads as follows.

Â We have box, true star followed by diamond true followed by true.

Â And what this represents is the following.

Â After any sequence of actions,

Â that's this box two-star, I can do another action.

Â Let's this true, a diamond true and in the end state only

Â true should hold, so there is no other requirements.

Â So after any sequence of actions I can do another action or

Â in other words this is sequence to saying there is no deadlock in my system.

Â 16:26

One example is the following, I have a machine, and

Â this machine has an action a, and then b, and an action c.

Â And the action a could be that a product enters the machine.

Â Action b could be that a product leaves the machine, and

Â c is that the product is actually processed in the machine.

Â And we don't want that a product that enters the machine

Â Leave the machine without being processed.

Â So, typically, we could have the requirement that between an action a and

Â b, the action c must happen.

Â 17:03

And how can we express that?

Â Well, actually we can express that with this formula.

Â Mainly after sequencing of exiting my machine,

Â if I do a a and this a is followed by a b without a c in between.

Â So between a and the b all kinds of exits can happen, but

Â not a c,then that is not desired.

Â So this expresses that between a and b, c must happen.

Â 17:38

So let's look at another example.

Â Suppose we have a heavy machine and

Â we have to put iron plate in the machine by hands.

Â The machine will actually detect that our hand is still in the machine.

Â After remove the hands, it will indicate that it is safe,

Â and then it will do this cutting action of this iron plate.

Â So an important requirement of course is that we

Â cannot do this cut action between a detect and

Â safe because this would mean that there is a risk that my fingers will be cut.

Â So how can we formulate that?

Â Well, in this particular case, it's convenient to reformulate

Â this in the following way, namely by saying that between a detect,

Â and a cut we always want to see the safe action.

Â 18:37

Namely, what we say is that if we do a detect,

Â followed by a cut without a safe In between?

Â That is completely undesired and that's not allowed.

Â And this formula actually represents that the machine is safe.

Â 18:54

Well, we can also have other requirements saying that it will

Â not cut before actually checking that a system is safe, so

Â in an initial state, before doing the safe action requirement

Â on this machine, we should first have a safety indication.

Â So doing the cut it out, the action safe in front, is not allowed.

Â 19:23

Okay, these were a number of safety formulas.

Â Now, let's look at number of life in the formula.

Â So suppose we have fire fighters and

Â if there is a fire they should appear.

Â And we can have a [INAUDIBLE] week variant of this property which you

Â probably would write down as the first potential candidate.

Â And it's not really enough.

Â So, what does this formula say?

Â It says whenever a fire action happens or the fire breaks out.

Â 19:58

And then, we write down diamond true is to appear, and

Â this means then there is a sequence of actions after which appear will happen.

Â So, if the fire breaks out,

Â there is the possibility that the fireman will appear.

Â There is a sequence of actions where they actually will appear.

Â But, they may not appear in most of all,

Â safe rests on the behavior.

Â 20:32

So, sometimes you would like to work.

Â Really say, that if a fire breaks out What ever happens within a finite number

Â of actions, the fireman will appear, and then we use this particular formula.

Â So this is the strict variant, and this is such an important formula, and so

Â tricky to understand that I advise you to learn it by head.

Â So what does it say?

Â After a fire appears, then as long as I will do

Â something different than appear action.

Â I will go on checking in a finite number often times and

Â I should always do some action.

Â 21:16

So, what I would like to formulate is that after an action a,

Â action b must unavoidably happen.

Â And this is the formal added we gave on previous slide, but

Â now with the a and the b.

Â And while this a part is not so interesting,

Â because that's relatively straightforward.

Â So if we end up in a state after the a,

Â where we can only do this b, then the formula becomes true.

Â 21:40

Namely, the right-hand side of the end says true, diamond true, true.

Â And because we can do an action this part of the formula is valid.

Â And the first part of the formula says whenever we do something different from b.

Â 22:01

Then we have to continue checking in the target state of that particular action.

Â Well, in this particular case where we have the state with only an outgoing b,

Â we do not have to check anything anymore.

Â So this formula becomes true,

Â if we end up in a state where we can only do b actions.

Â If we would do other actions, then because we have to

Â make the formula true, after a finite number of steps,

Â we are forced to enter in a state where we can do b action and only do b actions.

Â And it might that there are many more paths in the system.

Â And in any case,

Â we have to enter in the state where where we can only do these b actions.

Â 23:17

Now, you can see that this formula halts in

Â this particular case where we do an a directly followed by b.

Â But fairly often, you will see that the following happens namely between the a and

Â the b a rather irrelevant action can also happen.

Â Somebody can input something in another part of the machine under consideration.

Â Or it can be that somebody presses an alarm button,

Â and he can do this as far, as often, as she would like to.

Â So this is typically what you see?

Â And in this case, the formula is not true, because the b can

Â indefinitely be postponed, it is not guaranteed that the b will happen after

Â a finite number of actions, because you can do c indefinitely often.

Â 24:11

So, what one would like to say, is an alternative,

Â it's somewhat a weaker alternative, is the following, namely after

Â 24:23

doing the a as long as we have not seen the b, we can still do the b.

Â And that's often a convenient but weaker alternative,

Â there are stronger alternatives but they are a little bit more complex.

Â So typically what we can say is, that whenever we do a sequence of actions

Â followed by an a, followed by a sequence not containing the b.

Â So as long as we are not doing the b,

Â we will have the option to do the b.

Â And this is often, good alternative if you find that your first formula,

Â use trick formula does not hold due to these nasty loops, okay?

Â Let's do some exercises.

Â And let's look at this formula books true*a diamonds true b and

Â the question is, what does it mean?

Â 25:24

We look at this second exercise.

Â Here we have a minimal fixed point operator, and it is not b.

Â A books not b.

Â And the question, again, is, what does it represent?

Â If we write down true * r a b * c followed by false, What does it express?

Â Okay?

Â So what do we do?

Â We introduced action formulas.

Â Action formulas represent sets of multi actions.

Â 25:57

We extended it to regular formulas, and we showed a number of examples.

Â And I hope you started to realized that using regular phone

Â allows you to formulate quite a number of requirements that

Â you would encounter when considering behavior of systems.

Â