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.


Your Answer

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

Browse other questions tagged or ask your own question.