Sliding Window Abstraction for Infinite Markov Chains

We present ail 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 ail important role in the stochastic modeling of biological systems. We approximate the transient probability distributions lit 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 call 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.

Published in:
Computer Aided Verification, Proceedings, 5643, 337-352
Presented at:
21st International Conference on Computer Aided Verification, Grenoble, FRANCE, Jun 26-Jul 02, 2009
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa

 Record created 2010-11-30, last modified 2018-03-17

Rate this document:

Rate this document:
(Not yet reviewed)