So, the idea is that we should have very simple formalism which somehow captures or is close

enough to the notions of equivalence. I guess that in the lecture we have already covered

strong dissimilarity, weak dissimilarity to one, and trace equivalence. So ideally we

should have a formalism which is at least invariant under strong dissimilarity which

means that if you have two states which are strongly dissimilar they are as good as, well

maybe not identical, but they should be described by the same formulas. And on the other hand

if they are described by the same formulas, well at least in some cases it would be nice,

it would be almost like strongly dissimilar. And this should be also formalism which has

nice computational properties which is not too complex, like first of the logic for example,

you know, right, from glowing. So of course we could design first of the logic for label

transition systems very naturally. So for every a in the set of actions you think of

binary relation at a or however, whatever symbol you want to use for this. And then

you can write all sorts of formulas such like there exists x such that, or there exists

y such that x is in relation with y and y is not related by a to itself. So something

which should be, this kind of formula would be satisfied by this process if this is our

case, right. Fair enough. But is this a good formula? I mean first of all we know that

the first order logic is not decidable, I don't know if you remember this from glowing,

or whether this was mentioned somewhere. Do you remember what it means to be decidable,

or maybe it was used even during the notion of this lecture. And moreover I also said

that the formalism should have some connection with the notion of the trace equivalence,

process equivalence that we have, like be similarity. So let's consider on the one

hand, lay the transition system like this, and on the other hand something like this.

So, what is the difference between this two guys, this similar, actually it's the first

opportunity to play our simulation game. You remember the game characterization of simulation,

right? So the way in which you could show that these two guys, these two states, and

these two LDSs are similar would be by playing their game. So who wants to be attacker, who

wants to be defender? Who is in a better position here, attacker or defender? Well, defender.

Exactly. So okay, you'll be the defender and he'll be the attacker, so what do you want

to play? But you don't have much choice, right? Okay, it is more fun to play if you have at

least two or three transitions that you can make some good choices. Okay, that was just

what I can. We're not sure which transition system to choose, but yeah. Yeah, at any rate

we probably see that you are screwed, right? So what we generally choose, you can only

call A and then the opponent calls A, and then another A, A, A, A, and you keep playing

like this, it's clearly a winning strategy, which we generally value to do. So these guys

are a bit similar, but here this formula is satisfied because all these guys are not reflexive

in relation to A, there is no A loop, but this guy sees something which is a loop, A

loop, so this formula is not satisfied here. So for the logic, even though this is the

most standard formalism or language that we see in computer science, it's probably not

such a good candidate for formalism, which should be tailored for this reasoning about

C, about mid-nerve formalism or in general about concurrency and transition systems.

So what we are going to do, we are going to design very simple logic, which would be in

fact modal logic in this case. Have you seen modal logic somewhere? Was it mentioned? I

don't know. Did anybody add autologous for example? Okay, so this is what we are going

to call as whatever human and modal logic is discussing in some detail. So this would

be in particular, here we are doing it in a particular simple way, so we will have a

formalism without any variables even. So given a set of actions ACT, we are going to define

HNSE mid-nerve logic. I'm not sure, so far probably there were no formalisms or logics

in the lecture, so I can go for the Greek letters as well in the following way. We have

time for false and for true. Is this the one that you are accustomed to? False, true? And

then we can write conjunctions and disjunctions of our formulas. So correctly it would be