[MUSIC] So let's get started with this online course on quantitative model checking. It consists of five modules. And I like to switch between a modeling formalism and the logic you can use for model checking. So in this first module we'll deal with computational tree logic, and computational tree logic can be used to model check labeled transition systems. This first lecture is meant as an introduction to the subject. So, we use computational tree logic on transition systems for model checking purposes. What is a transition system? It is a model that includes states and transitions. Nodes represent states, can for example be the current color of a traffic light, or the current value of a program variables, or it can be the current value of registers and values of input bits. Then we have transitions and edges model such transitions. What can a transition be? It can be the switch from one color to another for the traffic light, or it can be the execution of a program statement, which changes your current value of the program variables. Or it can be the change of registers and output bits for a new input. So what is the formal definition of a transition system? Well, we need so called labeled transition systems, and the labels we need for model checking. And such a labeled transition system, which we abbreviate as an LTS, is a tuple, which consist of S, which is a finite set of states. T, as a transition relation from S to S, such that a tuple of two states is in this transition relation if there is a transition possible from the first state in the tuple to the second state in the tuple. And then finally we have the labeling function, L, which assigns one or more a finite set of atomic properties to each state S in the state space. Now, you might have seen other logics, for example, linear time logics. I can tell you that a CTL uses a branching time notion. So, what does it mean? It means that we have an infinite tree of states that represent the behavior of the system. So to say all possible executions of the model are in this computation tree. Then this computation tree is computed, so to say, by unfolding into a tree and a projection of all states to their labels. So this is an example of such a computation tree. And you start for a state S, this one for example, this is your starting state, it is somewhere in your label transition system. And then from this state you can take three transitions. And all these three transitions are shown here and each transition brings you to another state in the labeled transition system. And then you see from this state here you only have one successor, but from the other two states you each have two successors. Well, my space here is bounded so I cannot show you the whole computation tree. But you can imagine that it keeps going on, possibly until infinity. So this is the computation tree, which stems from the branching time notion. You start with a labeled transition system, with this formal definition I've shown you. From that you can derive this state graph plus the labeling. It's a visual representation of a labeled transition system. And then you decide whether you want to go for linear time or for branching time. Well, we only deal with branching time and this computational tree which unfolds. So this is what you use for CTL, but it's important to know that there's other possibilities, namely this linear time view, and then you would model check, for example, a logic that is called LTL. So, let's take a deeper look into CTL. CTL distinguishes between state and path properties. And a state property says which properties are true in which state. And the path properties say something about the validity of some or all path that originate from a particular state. And this difference is really important and it will continue to be important throughout this course. So if we want to check path properties, we need to know what a path is. And a path is a finite or infinite sequence of states here from S0, this is an infinite one, such that each two successive states are in the transition relation. So that basically only means that you can move from S0 to S1 in the labeled transition system, and so on. And this has to be true for all successive states. Now, how does computational tree logic look like? Let's start with the so called state formulas. State formula, capital Phi here, can be an a, an atomic property a. It can be the negation of a state formula. Or it can be the disjunction of two state formulas here, phi or phi. And then we have two more operators, one is the exists operator and the other is the for all operator. So exists says that there exists at least one path which fulfills a path property small phi. And the for all, obviously, does say something about the fact that all path fulfill this small phi. So how can a path property look like? We can have neXt and Until. And neXt says that, the next site starting from where we are now, fulfills this property, capital Phi, which is again a state formula, so pay attention here. And then the Until formula, phi until psi here, says that along a path originating in the state where we are now, phi holds along the path until psi holds. And again, Capital Phi, Capital Psi are state formulas. In a path formula, we reason about state formulas. So this is the definition of CTL, splitted in path and state formulas. What can we do with this? We can, for example, express eventually, as exists eventually phi or as for all eventually phi. And this diamond here, this means eventually. And what is the semantics? Well eventually translates to true until phi. Here in both cases the only difference is that once we have the exist and once we have the for all operator there. Something else we can do is the always operator. And always is this box. And always means that along a path for each state that we visit, this property phi will hold. And the always can be translated to here, eventually not phi, but be careful. We have to turn around the exist of all operator that is wrapped around this path property. So exists always phi, translates to not for all eventually not phi. And the same holds for the for all operator. So, for all always fine translates to, not exists eventually not fine. So eventually, always are important. They are often used in practice for property specification. Now, something else to be alert of is that you pay attention when you wrap path and state properties. So this, for example, exists not eventually not phi, is not a valid CTL formula. Because we said that exists is always followed by a small phi, which stands for a path property. And here we have the negation, which is a state property, yeah? So be careful that you always follow this syntax definition that I've given you. Now, some more examples. We can express reachability is basically the same as eventually. So simple reachability is the same as eventually, exists eventually psi here. So there is at least one path such that eventually we'll reach such a state psi. Then we have conditional reachability, uses the until operator, and it states that phi until psi. So it puts a condition on the first part of the path that we take until we eventually reach this psi state here. And then when we can express something like reachability from any state. Now from any state needs this for all always. And that means that for any state in your state space you will always, Find such a path such that you eventually reach phi here. So this is three forms of our reachability. We can also express safety properties. Again, we have a simple safety property, which is for all always phi. So that basically means that any state in your state space is safe or is such a phi state. And then again we can have conditional safety, and this one says that either it is safe, so for all always psi here, or for all phi until psi. So either any state is safe anyhow or from each state will reach a safe state via only these phi states. So that is safety, then we can say something about liveness. So here we want to ensure that from each state in your state space and again you see this for all always from phi. It follows that for all eventually psi here. So this means from any state in your state space, you will be able to reach such a live state psi again. And then we have fairness, and fairness is again a property for any state in your state space. So here you have for all always again, and then we have for all eventually phi. Yeah, and this basically means that [LAUGH] This is a bit difficult to express. So this basically means that for each state in your state space, you have the same property that you will be able to reach eventually, set a phi state. So this is form of fairness that we have here. So with these examples, I would like to conclude the first lecture. And if you want to know more about the semantics and the model checking approach, just keep watching. [MUSIC]