Verification of Infinite-State Systems with Probabilistic Behaviour - Abdulla, Parosh Aziz; Majeed, Asso Raouf; Amin, Sallah Hama (Sulaimani Journal for Pure and Applied Sciences, 2007)
We present a method for perforrnin g qwantitative onalysis of probabilistic sysierrs with infinite state spaces: given an initial state srrrr, a ilt F'of final states, and a ritional 0 >0, compute a rational p such that tr,.prouluullityofreachinge*oms;,xisbetweenandpr$'wepresentanalgorithmworkinginbreadth firsimanner to perform qfantitative'analysis of infinite state Markov chains, and provide sufficient conditions for termination of our algorithm'
Keywords: Markov chains; quantitative analysis; lossy channel systems