[MUSIC] So let's do the other probability operator now. The so called Time-bounded Until. Before we do that I would like to recall the semantics of this Time-bounded Until operator with you. So what does it mean? We want to check for a L-DTMC If this property phi until psi with a time on k holds or not. Well this path property small phi is fulfilled once a psi state is reached in at most case steps a longer path that consists of only psi states. On the other hand Phi is violated once a state is hit that is neither phi nor psi. And of course once we have reached the step limit k, we also violated the formula, if we hadn't reached a psi state. Let us formalize this. The probability that a state s fulfills such a formula is split up into three cases. The first case, we start in a state s that is a psi state. Well, if we start there, the formula is immediately valid and the probability is 1. On the other hand, if we deal with the state s, that is a phi state, and not a psi state, then we have a recursive computation. I'm going to show you, so here we have such a state s that is phi and not psi. And what we do is we accumulate the probability for all states s prime in the state space, and we multiply the probability to move from s to s prime with the probability to validate the formula phi onto psi, but now with one step less, so for k, -1. This is the second case and then in the third case, we are not in such a state and the probability is 0. So for any other state the probability is 0. Now if we want to apply this, we can solve this with a fixed-point iteration, but this is very cumbersome. So instead I'm going to show you a better way to solve this. And this is what we call the pCTL trick which reduces model checking the bounded until operator to a transient analysis. How does this work? Well, first we have to transform the DTMC that we are checking. And we make absorbing all psi states, because once we hit up the psi state we done in the formula holds. And we have to make absorbing all states that are not phi nor psi, because if we stumble upon one of these states the formula doesn't hold anymore. So we make these states absorbing, and then we check for reachability of psi in the transformed DTMC. And this reduces to transit analysis, and we have to accumulate the transient probability to be in a state that belongs to the satisfaction set of psi at time k. Then we compare this accumulated probability with the probability bound p. Either holds, then the formula is valid, or it doesn't hold and the formula is false. So let's take a look at an example. This is the property I would like to check. Up 3 or up 2 until down in utmost three steps. You've seen this already in one of the previous lectures. Now I'm going to replace up 3 up 2 by colors to better visualize the formula. So this is the DTMC we'll use. You see we have one red state corresponds to down and then we have green and blue corresponding to up 3 and up 2. And we have a white and a yellow state. Now, I have to make this DTMC absorbing in the sense that all the red states become absorbing and all states that are neither green or the blue or red are made absorbing. What does it mean to make them absorbing? It simply means we have to remove all the outgoing transitions. So let me do this for you. I have to get rid of this one. And I have to get rid of these two because white is neither green, blue or red. And also here in yellow I have to remove all the outgoing transitions. Now let's see whether I did this correctly. Yes, looks like it. So this is the transform DTMC which we use for the transient analysis. Now for the transient analysis, we need the probabilities on the edges and from that we derive the P matrix which you need to compute the trans-improbability distribution after three steps. Now the only problem is, now that I want to know for each state of this DTMC whether it fulfills that formula, because I need that for the satisfaction set. Now, I have to do the transient probability distribution. For four initial vectors and each time it represents another state as the only initial state. So this is how it looks and now I have to multiply these four vectors to P to the power of 3. And then, I obtained the transient probability distribution for each state as a possible starting state. Now this is fine but it is very cumbersome, so I would like to note that the so-called forwards computation requires a single transient analysis for each possible starting state. Now, if you want to know how to do this more efficiently, I would recommend to watch the next lecture. [SOUND]