A note on the attractor-property of infinite-state Markov chains

In the past 5 years, a series of verification algorithms has been proposed for infinite Markov chains that have a finite attractor, i.e., a set that will be visited infinitely often almost surely starting from any state. In this paper, we establish a sufficient criterion for the existence of an attractor. We show that if the states of a Markov chain can be given levels (positive integers) such that the expected next level for states at some level n > 0 is less than n for some positive , then the states at level 0 constitute an attractor for the chain. As an application, we obtain a direct proof that some probabilistic channel systems combining message losses with duplication and insertion errors have a finite attractor. Key words: Theory of computation; Attractors in Markov chains; Verification of probabilistic systems; Lossy channel systems.

• Type: Journal
• Year: 2006
• Where: IPL
• Authors: Christel Baier, Nathalie Bertrand, Ph. Schnoebelen
• Keywords: Attractor, Finite Attractor, IPL 2006, Markov Chains