Decisive Markov Chains

We consider qualitative and quantitative verification problems for infinite-state Markov chains. We call a Markov chain decisive w.r.t. a given set of target states F if it almost certainly eventually reaches either F or a state from which F can no longer be reached. While all finite Markov chains are trivially decisive (for every set F), this also holds for many classes of infinite Markov chains. Infinite Markov chains which contain a finite attractor are decisive w.r.t. every set F. In particular, all Markov chains induced by probabilistic lossy channel systems (PLCS) contain a finite attractor and are thus decisive. Furthermore, all globally coarse Markov chains are decisive. The class of globally coarse Markov chains includes, e.g., those induced by probabilistic vector addition systems (PVASS) with upward-closed sets F, and all Markov chains induced by probabilistic noisy Turing machines (PNTM) (a generalization of the noisy Turing machines (NTM) of Asarin and Collins). We ...

• Type: Journal
• Year: 2007
• Where: CORR
• Authors: Parosh Aziz Abdulla, Noomene Ben Henda, Richard Mayr
• Keywords: Coarse Markov Chains, CORR 2007, Education, Infinite Markov Chains, Markov Chains