Stability and attractivity of absorbing sets for discrete-time Markov processes

Absorbing sets within the state space of a general discrete-time Markov process have been shown to play a crucial role for the model-checking of model specifications over an infinite time horizon. Infinite-horizon specifications such as probabilistic invariance, reachability and reach-avoid have formally been characterized and computed based on this structural property of the model. This paper further extends these recent results by investigating stability properties of the model over absorbing sets. Theoretical results are developed to study attractivity properties of such sets, and the outcomes are applied over a case study.