[MUSIC] Welcome again. This time I will speak about identities on modal formulas, a technique to show that modal formulas are not equal. And I will also spend some time on the distinguishing formulas. We recall from our courses on propositional logic, there are lots of formulas that actually express the same, and that are lots of identities among expressions. So let's just review a number of them. We for instance, know that we can exchange the left and right-hand side of an and as is shown by this commutativity identity. We know that we can put the brackets in every way we want around an and, and that's associativity. If we have phi and phi, then we know that this is just expressing the same as phi. And not true = false. Phi and true = to phi. Phi and false = false. We know that the and is distributing over the or, as is the or distributing over the and. Negation can be distributed over the and, but then the and is replaced by the or. And we also know this equation that says that if we have two negations, we can simply remove such a negation. So we have also identities of this kind for modal logic. So let's look at a few. And we do that by looking at this formula a true. And the question is what does it express? So if we try to extend that, we can look at the state with an outgoing a transition. And then the requirement is that after any a transition, true should hold. Well, we know that true does not add anything. True is always valid so it does not put any requirement on the target state. So what we say is that if there is an a transition, we have no requirement on the target state. And that does really not put any requirement on the state as itself if there are outgoing a transitions. If there is no outgoing a transition, then we also know that a true is equal to true. So what we see is that this formula, a true is equivalent to true. And this is a particular pattern, namely a box modality, followed by a true can always be replace by a true. And this means because I so now and then see people writing down the box modality followed by true, and then they believe this means something else than true. So this means if you see the box modality followed by true, you should be aware that you are not writing down anything useful. So let's look at another formula, namely diamond modality, a followed by false. So, what does this say? This says that you have states that there should be an a transition to a particular state, and that state should satisfy false. But we know that no states satisfy false. So we express here that there should be a state, an a transition to a state that cannot exist. Or in other words, this is a property that cannot hold for any state. So what we know is that a false is equivalent to false. Here, we have a slightly more complex pair of formulas, namely diamond a followed by an expression with an or. And we could ask ourselves, are they equal? Or are they different? Well, they are equal, and this can be seen as follows. Suppose that we have a state for which the formula at left holds. Then we know that there is an outgoing a transition and that the end states of the end state should either, in the end state, either phi should be valid or psi should be valid. So if phi is valid, then we can see that the right formula is also valid because we have an a transition towards a state where phi holds. If psi is valid in the end state, then we see that formula at the right is also valid. So if the formula at the left is valid, the formula at right is valid. And in the same way, we can see that if the formula at the right is valid, and in that case either a phi should be valid. Or diamond a psi should hold, we can see that the formula at the left is valid. So we can see that we have this identity saying that diamond modality distributes over the or. And completely similarly, we see that the box modality distributes over the ands. And we actually know that, under very particular circumstances, the diamond modality also distributes over the and, and the box modality also distributes over the or. But this is not completely trivial. Okay, we can also look at some formulas that are not equal. And then the question is, how can we convince ourselves that they are actually different? And the trick is the following. Namely, We write down two. We want to have two transition systems, one for which phi 1 is valid and phi 2 is invalid. And the other for which phi1 is invalid and phi2 is valid. So let's first look at the left and try to construct it. So what we need is a formula for which phi1 is valid, and phi1 says that we can do an a transition like this. After which, either b or c must be possible. So let's do a b. So now phi1 is valid. Unfortunately, phi2 is also valid because after every a transition, we can do either a b or c. So in particular, we can do this b. And that means that if you want 5.2 to be invalid, we have to add something. And what we have to add is an a transition, after which we cannot do a b or c, and that's done like this. So now, phi2 is invalid, and we must check that phi1 has not become invalid, also. But what we can see is that we can still do this a followed by b, making phi1 valid. This extra a does not add anything to the validity of phi1. So if we now look at the other example, then we have this state as the counterexample, namely, phi1 is invalid. Why? Because we cannot do an a step, and phi1 says that we should be able to do an a step. So that's okay. And phi2 is valid because for all a transtions that we can do, something holds. And that holds trivially because there are no a transitions. So, these two examples show that the formulas phi1 and phi2 are really different. If you go back to Hennessy and Milner and we look at their original motivation, then we see that they made the Hennessy-Milner logic to characterize strong bisimulation. Especially they were after this theorem saying that if two states s and t are strongly bisimilar, then all formulas are either valid for s and valid for t or not valid for s and not valid for t. And the reverse also holds if you have two states for which exactly the same modal formulas hold, then the two states s and t should be strongly bisimilar. So there are two usages of this theorem. Namely, if we have a fairly complex transition system and we would like to make it a little bit smaller, but we would still like to maintain the validity of model formulas. Then we can safely reduce the transition system, modulo strong bisimulation. There's an other in my opinion even more spectacular use of this theorem. Namely, if we have two transition systems that are not bisimilar, and let's take two that you already know. For instance, this one and this one. Then we know that there must be a formula that is valid for one transition system, but not valid for the other. And such a formula is called a distinguishing formula. And what's the distinguishing formula in this particular case? Well, there are many candidates, but this is an option. Namely, the formula that says that you can do an a after which a b and a c are possible. And we can see that this is valid in the transition system at the left. But it is not valid in the transition system at the right because we can do this a at right, but we cannot do both b and c in any of the reachable states. Okay, let's do an exercise. If you have these two formulas, are they actually expressing the same? Now we look at these two transition systems. Can we find a distinguishing formulas for these transition systems? And if so, how does this distinguishing formula look like? Okay, what did we do? We formulated a number of identities on propositional logic and especially on modal formulas. And these identities are really helpful if we want to understand modal formulas. We will find out that modal formulas are not very easy to comprehend, and it is really sometimes useful to transform them to an equivalent but different form, and try to enter this different shape. We also showed how we can understand that two transition systems after two modal formulas are actually different by giving a transition system showing the difference. And we introduced the notion of distinguishing formulas. The next lecture will be devoted to dualities in logics. Especially for modal logics, it is useful to be aware that these dualities exist. See you next time. [MUSIC]