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.