3
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.