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

Question

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.

Answer 1

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$.