Sliding Window Abstraction for Infinite Markov Chains

Window Abstraction for Infinite Markov Chains Thomas A. Henzinger1 , Maria Mateescu1 , and Verena Wolf1,2 1 EPFL, Switzerland 2 Saarland University, Germany Abstract. We present an on-the-fly abstraction technique for infinite-state continuous-time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time inby solving a sequence of dynamically constructed abstract models, each g on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstracbe computed, and the precision of the abstraction re...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Thomas A. Henzinger, Maria Mateescu, Verena Wolf
• Keywords: CAV 2009, Continuous-time Markov Chains, Finite Markov Chain, Formal Methods, Infinite Markov Chains