[MUSIC] Welcome back to the course on Quantitative Model Checking, and let's do some more model checking today. Namely, we check the continuous stochastic logic, which is abbreviated as CSL on CTMCs. And this first lecture is meant as an introduction to model checking CSL. So, first of all, we have to revisit the definition of CTMC. And recall that a CTMC was defined as a tuple consisting of the state space S, and the rate matrix which gives the rate with which you move from one state to another. And with that rate matrix, we could do some calculations. We could compute the so-called generated matrix instead. But we could also compute the so-called exit rates for a state S, which accumulates the outgoing rates for that state S. Now, what we have to do if we want to do model checking, we have to add the so-called labeling function L. And L assigns zero or more atomic properties to each state. And these atomic properties, they come from the set AP. Now, continuous stochastic logic consists of state-formulas and path formulas, just as PCTL. Let me start with state formulas. This first part, you recall, it's the same as CTL, PCTL where you have an atomic property a. You can negate, you can disjunct properties. And recall that with negation and disjunction, you can also formulate conjunction and other properties. Now what is new is these two operators, the steady state operator and the probability operator. The steady state operator states that the CSL state formula capital phi holds in steady state with a probability that matches this probability bound P. And the probability operator states that each path that starts in a certain state S fulfills this small phi, which is a path formula with probability p. Now, recall that the CTL quantors exist and fall, can be rebuilt, so to say, with the CSL ingredients, using the probability operator. And once we do greater than 0 in order to mimic the exist quantor. And we do greater or equal to 1 if we want to mimic the all quantor. Now, moving from state formulas to path formulas. A path formula is always indicated with a small symbol here, just for notation and convenience. And you have the so called next operator. And the until. The until operator you, of course, know. The only difference is that now the time bound here is an interval from real time. So we have t0 has to be smaller or equal to t1. And the same here for the next operator. Now, what is the semantics of these operators? Well, next means that the next state is reached at a time t from this interval from t0 to t1. And it fulfills phi, capital phi here, again, is a state formula. Now, the until operator means that along the path, first phi holds. There's a phi missing. So here, a phi holds along the path until psi holds, and this switch from phi states to psi states has to take place at some time t from this interval between t0 and t1. So this is path formulas. And they also, in a sense, match the CTL operators, next and until. The only difference is that now we have these time bounds that come from real time. Let's take a look at an example. Well, this model you've seen before, it's a triple modular redundant system. And now we're going to formulate a couple of CSL formulas for this. Let's start with state formulas. So, is the probability that the next state is down? Sorry, is the probability that the next state down is reached within three time units? Smaller than 20%. So let me write this down. I need the probability operator, has to be smaller than 0.2. And then next, down, and now what is missing is the time interval, and that has to be from 0 to 3. Now, please note that often instead of 0 to 3, I will use something like small or equal to 3, and it has the same meaning, of course. Another state formula, the steady-state probability of being in state up0 is at most 10 to the power of -1. So for this, we need the steady-state operator, smaller than 0.1, and we want to be in up0. Next one. At least 99% of time, at least two processors are operating. This is, again, a steady-state formula. It has to be greater than 0.99. And now, at least two processors translates to up3, or up2. Yeah, and here you go. These are some examples for CSL state formulas. Now, let's take a look at path formulas. The system is going down between 10 and 30 time units. So this is an until. And I don't specify a property that has to hold before the until, so this is true, true, until, down. And now the time interval, that is between 10 and 30. Now, pay attention. This is a path formula, so I don't write the probability operator around because wrapping this probability operator would turn it into a state formula. Another one. The system is going down in 10 time units after continuously operating with at least two processors. Now this, again, is an until formula. But now I require that the system has been continuously operating with at least two processors before it is going down. So this is the property that goes before the until. And that is, again, up3 or up2 until down. Now in 10 time units, so this is the time bound. And again, this is the path formula. So let's be a bit more formal. In order to define the semantics of the time bounded until operator for CSL properly, we first need to take a look at the definition of path. So what is a path in a CGMC? Well, such a path, sigma, consists of states S0, S1, S2. And then the timing in between, and that is given here by t0, t1, t2, and so on. So this first path here is an infinite path. And what we require is that for each successive states, Si and Si + 1, there is a positive entry in the rate matrix. Yeah, because otherwise, there cannot be the step from Si to Si + 1. Then sigma i equals s, denotes that this is the i + 1 state of that path sigma. Then, we take a look at the time we spent in a state Si here, and this is given by the small delta. It takes as arguments the path sigma and the number of the state, so the ith state. Sorry, the i + 1 state. And this is then ti. So ti is the time we spent there. Then we have i as the smallest index for which time is small or equal to the sum of the amount of times that we've spent in those states so far. So this you can use to tell you in which state you'll be at, at time t. Now, sigma at t is sigma i. And that is exactly the state that we occupy at time t. And note that this i is the same as this i up there. So now that we've looked into paths, we can take a look at the semantics of CSL. So again, we have the satisfaction relation, and this is defined as this for the propositional part of CSL. That's all, you will recall this from CTL and PCTL. Now, this is the new part. Let's start with our steady-state operator here. Well, this is easy. It states whether the steady-state probability to be in a phi state matches this probability bound p. A probability operator, the same story, we need this probability here. And now the question, of course, is how do we compute this probability? And that depends on the choice of the path operator that we use inside. So here, see there's a difference. Here we check whether a path satisfies a CSL path formula. And here, we check whether these states satisfy the CSL state formulas. So coming back to the path operator, here the next is fulfilled if sigma 1, that is the next state on my path, and is defined, so it needs to exist. And this state, sigma 1, satisfies phi now, because that is what we require for our next state. And then, one last thing to check. We have to check that we reach this state in the time interval i. Okay, moving to the until operator. So first of all, there needs to exist a time point that is in the time interval i here. And then, the state of my path at that time instant t has to satisfy psi. And for all the time instances before, that is for all t prime, between 0 and this t. The states, at these instances t prime, have to fulfill phi. Yeah, that is my until, phi until psi. So now you've seen the semantics of CSL, state and path formulas. And if you want to know how to check these things, I recommend you keep watching this lecture series. [MUSIC]
