[MUSIC] In this lecture, I will show you a simple, straightforward logic, namely Hennessy-Milner logic. Here we see the pictures of Robin Milner and Matthew Hennessy. So, Robin Milner is a person that we have already seen a number of times. Mitchell Hennessy was a PC student of Robin. And they, together, made what is currently called the Hennessy-Milner logic. And their purpose was to characterize strong bisimulation with a logic and they came up with this particularly elegant solution for that. So what's Hennessy-Milner logic? And I present the syntax here using Backus-Naur form. So a formula can either be true, and true is the logical formula that's valid in any state. It can be false, false is never ever valid in no state. We can use a negation. The ands, the or well known from logic and we have two special operators namely, the diamond modality a phi. And this says that, you can do an a in a particular state after which phi should holds and box modality. And that says that whenever you do an a in a particular state, phi should hold afterwards. So when is a Hennessy-Milner formula valid? So we take a formula and a state and we say that this formula is valid in a particular state. And often we do not mention the state explicitly but then it's generally the initial state of the system that we consider. So we can say that true is a formula that's valid in any state. False is the formula that's never valid for any state. If we know that phi is not valid in a state, then not phi is valid in a state. And in the same way we can say this for and if we have the formula phi1 and phi2 then this formula is valid. If phi1 is valid in this state and phi2 is valid. And reversely for the or, phi1 or phi2 is valid in this state, if either phi1 is valid or phi2 is valid. And of course they can also be both valid in that state. And we also have the two modalities, the diamond modality and the box modality and I will spend the next slides on explaining these. So we have the diamond modality. And this says that. And so show a phi is valid in a state s, if there's a transition from s to a state s prime. And a transition such that phi is valid in s prime. So typically if I have a state s and I want to make this formula diamond a phi valid in s. Then there must be an outgoing a transition to a state s prime, where phi is valid and that is enough to make diamond a phi valid and can be more complex. We can have a state with an outgoing a to a state where phi holds and then already diamond a phi is valid but there can also be more outgoing a transitions to states of which we have no idea whether phi is valid. And it can even be outgoing transitions labelled with other actions than a, for instance b, and they are of no concern for our modality, a phi. Okay, so let's look at this small example. If we write down diamond a, diamond b, true, is this, what does this express? So, what it expresses is that you have a state s and in this state s it should be possible to do an a. And then you end up in a state where [b]true must hold. So from this resulting state, we have to be able to do a b, and then we end up in a state where true must hold while true is valid for any state, so that doesn't put any requirement anymore. It can be that we have more transitions and that does not really matter at all. It's enough that we can do an a and a b from the state s. So actually what we say is there is a trace, a b, from state s, using this model formula. We can also look at this mode of formula, where we say diamond a followed by. Diamond, b true and diamond c, true, so what does this express? Well, let's try to understand this in terms of a label transition system. It should be possible to do an a where b true and c true should hold. And that means that we should be here, that we should be able to do a b from this resulting state and a c. And this is enough to make this model formula true. We can also change our transition system a little bit. Take these outgoing a from the initial state and ask ourselves when this model formula holds from this transition system. Well, what we see is that we can do an a from the initial state. But then we end up either at the state of where we can do b or at state where we can do c. But we don't have a resultant state where we can do both a b and c. So what you see here is that this model formula is not valid for this transition system. We can change our transition system a little bit, by adding an extra b to the right branch. And what we see here now is that we have an a transition going to a single b, but this does not help to make this model formula true. But we have also an a going to a state to be kind of both b and c. So in this particular case the model formula is also valid. And this is what is the formula, this is what the formula expresses. Namely there is an a after which a b and c are possible. So we can also look at the box modality. So the box modality is valid in state s. When for every a that you can do phi holds afterwards. Or put in other words for all state s prime such that we go from s with an a stat to s prime, phi should hold in s prime. So expressed in the transition system if we have a state s, and we have only one outgoing transition a. And phi holds after doing a, then box a phi is valid. And then we have a state s and we have more outgoing transitions after which phi is valid. So for this one, and for this one, then we can say that [a] phi is valid. And it doesn't really matter if we have other transitions than a transitions. So generally I'm not even considering them. They are irrelevant for this formula. There is one special case where box a phi is valid and that's this case. If I have only a single states without any outgoing any transitions, then a phi is valid. Namely for all outgoing a transitions and the I know outgoing a transitions. Phi holds at the end. And you can see that independent of how phi looks, this formula is always valid for any transition system of any state without outgoing a's. So let's look at a few formulas with box modality. So if we have box a, diamond a, true as a formula. What does that mean? And just to understand this transition system with two outgoing a's in this not so relevant b. This says that if I do an a, I end up in a state where diamond a should true hold. So after doing any a, I must be able to do yet another a, so an a should be possible there and an a should be possible here. And that is exactly what it says. It says after any am another a can be done. Okay, look at this example and this is an example that you will see more often. What's the meaning of box a false? Well if I have a state with an outgoing a transition and what we see is that after this outgoing a transition, false should hold. But we know that false does not hold in any state, so if there's an outgoing a transition, we have an impossible situation. And there's only one way to make this formula valid and that is by forbidding that an a can be done. So actually, It's only valid in a state without outgoing a transitions. And this is the meaning namely box [a]false is valid in a particular state, if an a action is not possible in that state. Okay, let's look at the number of exercises. If we have this model formula consisting of five times diamond a, then does this formula holds in a state s? Here we have the second exercise. If you have the formula diamond a true or diamond b true or diamond c true. Then does this formula holds and I give four possibilities. And now the third exercise we have box a, box b, box c, folds. What does it express or differently, when is it valid in a state s? Okay, so what did he do? He introduced Hennessy-Milner logic. And with Hennessy-Milner logic we can express elementary properties of labelled transition systems. And Hennessy-Milner logic consist of the standard logical operators from propositional logic. And we have two modal operators, namely, the diamond modality, diamond phi, and the box modality, box [a] phi. In the next lecture, I will show you a number of identities among Hennessy-Milner formulas. Thank you for watching. [MUSIC]