# Algorithm for computing $Pr[s \vDash C \bigcup^{\geq n} B]$ for probabilistic verification

I'm having some difficulty trying to come up with an algorithm for computing $$Pr[s \vDash C ~\bigcup^{\geq n} B]$$ given a finite Markov chain where $$S$$ is the set of states, $$s \in S$$, $$B,C \subseteq S$$, and $$n \in \mathbb{N}$$ where $$n \geq 1$$.

I have algorithms for computing $$Pr[s \vDash C~\bigcup~B]$$, $$Pr[s \vDash C~\bigcup^{\leq n}~B]$$, and $$Pr[s \vDash C~\bigcup^{=n}~B]$$. Instead of going down to the Markov chain itself I was thinking of using a combination of these algorithms to calculate $$Pr[s \vDash C ~\bigcup^{\geq n} B]$$, however, I'm worried about overcounting as it is not necessarily true that $$B$$ and $$C$$ are disjoint.

I am using the Principles of Model Checking book by Baier and Katoen.

To compute the probability for $$\geq n$$, you first compute the probability for an unbounded until and subtract from it the probability for $$\leq n-1$$. If you compare the sets of paths these formulas represent then you will that they are indeed the same. You start off with a set of all paths satisfying "reach B via C", let's call it $$T$$. From this set, you remove any paths where B is reached in $$\leq n-1$$, let's call it $$U$$. So the set of paths where B via C is reached in $$\geq n$$ steps is represented by $$T \setminus U$$. Using properties of probability measures, you can write $$Pr(T\setminus U) = Pr(T) - Pr(U)$$.
You can safely assume that $$B$$ and $$C$$ are disjoint without loss on generality. If they are not, then reaching a state from $$B \cap C$$ satisfies the "until", so you can just consider $$(C\setminus B) \bigcup B$$.