## Sliding-Window Abstraction for Infinite Markov Chains

*Maria Mateescu,
Thomas A. Henzinger,
and Verena Wolf*

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
instances by solving a sequence of dynamically constructed abstract
models, each depending 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 abstraction
can be computed, and the precision of the abstraction refined when
desired. We implemented the algorithm and demonstrate its usefulness
and efficiency on several case studies from systems biology.

*Proceedings of the
21st International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 5643,
Springer,
2009,
pp. 337-352.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2009 Springer.