[MUSIC] Nice to see you again in this third MOOC on modal logics. In the first MOOC, you learned about transition system as a model of behavior. And you assure behavioral equivalences as a way to reduce this behavior. In the second MOOC, you learned how to model complex behavior using process algebra and data types. And in this MOOC, you will learn about requirements and how you can formulate them using modal logics. This is an example of the alarm clock that you have already seen multiple times. We had this SetAlarm action to set alarm, SoundAlarm action indicating that the alarm was sounding and the ClearAlarm action. And what we can ask ourselves are whether this behavior is satisfying certain requirements. And a typical instance of a requirement is the following namely, does the alarm clock have a deadlock? So yet it stops and cannot do anything anymore are complex. If it's the case that if I set the alarm, the SoundAlarm will always take place unless I clear that with the ClearAlarm. And that's, of course, the behavior that we expect from an alarm clock. All these properties can be modeled using modal logics. So what we will do in this MOOC is introduce a modal logic to specify behavioral requirements. Concretely, we will start out the Hennesy-Milner logic, which is still quite a simple logic. We extended the fixed point operators. This is quite tricky and not so easy to comprehend, but extremely powerful. We show the notion of regular formulas, and it makes it easy to specify behavior. And we add data to this whole setup. And if we will have that data, you will have the most powerful logic available currently, much more powerful than well-known logics such as LTL or CTL. The next question is that if we have this logic and if we verify the number of requirements, how can we actually check that a model formula is valid? So this is conveniently done by tools, but you can also do it by hand by translating them to parametrized Boolean equation systems. In the next lecture we will introduce Hennesy-Milner logic. [MUSIC]