2
$\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$

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.