[MUSIC] >> So let's take a look of the general motor checking routine for CSL and let see how the Time-bounded Next operator in motor check. So first of all, model checking CSL, if we want to see whether a state s of a CTMC satisfies a CSL formula phi. We have to do a recursive computation of the satisfaction set of phi and then we can simply check whether that state belongs to the satisfaction set or not. For the non-stochastic part of CSL, model checking just goes as for CTL. Question that remains is how to compute the satisfaction set for the stochastic operators? Well, this is the general model checking routine. What you see is the none stochastic part here and then the studies that operator, and the probability operator once for next, and once for until. So if you want to implement your own sears or modern checker, this is so to say, the main file which you would use to in order to distinguish between all the cases of operators that you will see. Now, let's go to time next. If you want to know whether a state s satisfies the probability operator wrapped around the next, what are time interval from a to b. What we have to do is we have to compute the probability that a path starting in s satisfies next phi where I here is the same as the interval from a to b and then we have to compare this computed probability with the probability bound P. So, how do we compute this probability? Well, this is it. It consists of two parts. Here, we compute the probability to leave state s in the time interval from a to b. Recall that 1 minus E to the power of minus Est gives you the probability to leave state as before time t. So what we do here is we subtract the probability to leave before time b minus the probability to leave before time a. But we do not simply want to leave the state, we want to move to a state, s prime that satisfies phi. So we have to sum over all states s prime in the satisfaction set of phi and then we have to sum the weighted rates, so to say. So, the rate to move from s to s prime divided by the exit rate. And once we have computed this, we compare whether this probability matches the probability bound p. So, let's put this into practice and I brought you an example. It's the example of an absent-minded professor. She has two umbrellas and she regularly commutes from the WWU Munster to the UT in Enschede and back, of course. So she only takes an umbrella if it rains and it rains with probability 0.6, and we want to build a CTMC model. So, we need to consider state residence times. Now let's assume that the time I spent in Munster is the the same as the time I spent in Enschede, so we can use the same rate for all states, which is five here in my example. Now if I want to model this, I am going to model only the number of umbrellas that are at my disposition. So either I have zero umbrellas or I have two umbrellas, or one. So I have three states, 0, 2 and 1. And if I'm going to a place with no umbrella, I have no choice, but I just commute without an umbrella and then to a place where I have two. Then if I am in a place with one umbrella, I can either take it if it rains, then I commute to a place where I then have two umbrellas or I leave the umbrella and commute to a place where I have one umbrella. So if I'm in the place with two umbrellas, I take one if it rains or I leave them if the Sun is shining. So you would be tempted to simply add the the probability for rain or no rain here, but we want to have a CTMC, so we have to multiply with the state residence time five. So this is the resulting CTMC for this example and now, which property are we going to check? Well, of course, we want to avoid the scenario where I get wet. [SOUND] So, this is the property we are checking. We want to ensure that with probability at least 0.9 in the next step, I am in a safe state. And as time mount, I used zero to one for one day. What is a safe state? Well, a safe state is a state where I have at least one umbrella. So, these are indicated in green here. How do I check this property? Well, for convenience, I imported the formula that I just showed you and now we have to fill in the values of this example here. So, I'm going to check first for stage two. So, the exit rate of stage two is five. So e to the power of -5 times 0 and 0 corresponds to that 0 here minus e to the power of minus 5 times 1 and then times, well, the sum of all the rights that bring me to a safe state. Well, starting from two, there's only one safe state reachable in one step and that is this one with rate three. So times 3 divided by the exit rate, which is 5. So, let's do the computations. E to the power of 0 is easy, that I can do myself. E to the power of -5, somebody with a calculator. Yeah, here. >> 0.006738. >> Thank you. Times 3/5 and this is 0.993 and now my computation is still loosing me again, so let me cleans it up for you. The result is 0.59, which is of course is much lower than the probability bound of 0.9, which we wanted to check for. So state two does not satisfy the property, you can do the same thing at home if you want for stage zero and one. And what you'll see is that the satisfaction set of this formula consists of two stage namely, S0 and S1. [MUSIC] So, let's check for the weather. Yeah, it rains. [SOUND]