Sliding-window abstraction for infinite Markov chains Conference Paper

Author(s): Henzinger, Thomas A; Mateescu, Maria; Wolf, Verena
Title: Sliding-window abstraction for infinite Markov chains
Title Series: LNCS
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 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.
Conference Title: CAV: Computer Aided Verification
Volume: 5643
Conference Dates: June 26 - July 2, 2009
Conference Location: Grenoble, France
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2009-01-01
Start Page: 337
End Page: 352
Sponsor: The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840.
DOI: 10.1007/978-3-642-02658-4_27
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work