[MUSIC] So now you know how to model check the steady-state operator and the next operator. Let me show to you in this lecture how to model check the Time-bounded until. How does it work? Well, if we want to know whether a state is in the satisfaction set of a path operator that is repped inside the probability operator, we have to compute the probability that from that state the path formula phi matches the probability bound p. For a time interval from zero to t, this probability is the least solution of the following set of equations. First of all, if s is upsized state we are done. We've reached a goal state, and this property is fulfilled with probability 1. On the other hand, if s is not upsized state, nor a phi state, we have violated the property and this probability is zero. For all other cases, that is all states that are neither phi nor up psi, we have to do a little bit more work in order to compute this probability. So what we do is we take the integral from zero to t, and this t comes from the time bound here. And then, we have to sum over all states s prime in the state space. Where do we sum? Well, the rate to move from s to s prime before time X, and we multiply with the probability that the state s prime will be moved to satisfies the property phi unsub psi. Now we have to change the time bound slightly, and it now goes from zero to t minus x. Why is that? Well, we've spent x time units on the transition from s to s prime, and that leaves us t minus x time units for the rest. So this is what is written here. The first part is the probability to move from s to s prime, and the second part is the probability that s prime fulfills this property. Now, the question you might have is how to compute this integral. Well, there's several methods for numerical integration. For example, the trapezoidal method. Unfortunately, this is not very efficient. So, the computation is time consuming, especially for large state spaces, and moreover, the run-time heavily depends on the required accuracy. Finally, the accuracy you can achieve might not be enough for your model-checking purposes. But there is a way out. If you think about model-checking the time until in PCTL, you recall that this property is fulfilled once a psi state is reached before time t on a phi path. On the other hand, it is violated once a non-phi nor psi state is reached before time t. And just as for model checking a time-bounded until CTL, we're also able to reduce the case to a transient analysis. And how do we compute the transient probabilities on the CTMC? Well, we use uniformization. And before I'm going to show you an example, let me formalize this for you. So, we move from the Markov chain m, to a Markov chain where all size states, that is, the goal states, and all violating states, that is, all non-phi and non-psi states are made absorbing. If I combine the both, I obtain a chain m, where not-phi or psi states have been made absorbing. So then, for any CTMCM, I can compute this probability we're after as the sum over all states, s prime, that fulfills psi. And what do I sum up? I accumulate the transient probability to be in that state, s prime, at time T, and this transient analysis is performed on this reduced Markov chain where non-phi or psi states have been made absorbing. Yeah, so this is the idea. This idea has been introduced in this seminal paper, Model Checking Algorithms for Continuous-Time Markov Chains. And it posed a major breakthrough in the research on continuous time model checking. So let me show you the premise example. It is a model you've seen before, the triple modular redundance system. And again, I've used colors to visualize labels. So, we want to check where the green or blue until red, and that has to happen in the time interval from zero to 3. Now, what do I have to make absorbing? Well, all red states. There is only one, so this. And all states that are not green or blue or red. And that leaves the white one and the yellow one. This is how the transformed Markov chain looks like. And then I perform uniformization. So I compute the uniformized DTMC. For that, I perform a transient analysis. In this case, up to time 3. And then, I accumulate the transient probabilities for all gold states. Okay, for the time bound until and real time, there are more options. Next to the time interval from zero to t, you can also look at the more involved case where we have a time until from t to t prime. And I just want to show you the idea. So, for any path that fulfills such a time-bounded until from t to t prime, we know that phi has to hold continuously up to time t. And then, the suffix of the rest of the path that starts at time t needs to fulfill phi until psi. But now, I have to change this interval slightly so it goes from zero to t prime minus t. So a length of the interval stays the same, just the starting point has shifted. If I want to check this, I can reduce it to two subproblems. The first checks whether always phi holds up to time t. And this is a simple transient analysis up to time t where I make all states that are non phi absorbing. Out of this sub-problem, I obtain a probability distribution, pt. And this I need in the second problem. because here, I need to check phi psi for the interval from zero to t prime minus t, with the starting distribution pt. And that is what I obtained from the first problem. So this goes here. Well, this problem you've seen before. It's a simple time bounded until with a time bound that starts at zero. So this works exactly the same as what I've shown you before. So, this is just for convenience so you know how this works. We won't use this in this course. Let me give you a quick overview of model checking CSL. What have we seen so far? Well, the prepositional part of CSL works just like CTL. Then we have the steady-state operator. For that, we need a graph analysis plus a linear system of equations needs to be solved. For the time bounded next, we do a matrix vector multiplication. You might be surprised because this is not what I've shown you. But the approach I have shown you can be easily extended to check, again, for all states in one go with a backwards computation, just as in PCTL. And then, there's the time-bounded until, which can be reduced to a transient analysis. And this reduction to a transient analysis is a very positive thing. It comes with a lot of advantages. It allows to use efficient techniques such as uniformisation. The number of iterations can be determined a priori. And the CTMC is only made smaller in this process of transformation. So you will have less entries in your matrix. And finally, uniformization can be carried out for all states simultaneously. So, you do this complicated computation once, but then you're able to have the whole satisfaction set for that property. [MUSIC]