Rare-Event Guided Analysis of Infinite-State Chemical Reaction Networks

Probabilistic Model Checking (PMC) is a valuable tool for automated analysis of systems exhibiting stochastic behavior. However, the effectiveness of PMC algorithms is limited to systems that can be modeled by a finite state-space. Chemical Reaction Networks (CRNs) are commonly used to describe biochemical systems. Since there are usually no upper-bounds on the population of species in a CRN, they can only be modeled as an infinite-state stochastic model. This paper proposes a new approach that can analyze infinite-state CRNs by bounding their state-space. For a property indicating that the probability of the event of interest is less than a certain threshold value, the objective is to generate a bounded range on the population of each species in the CRN such that this bounded CRN already retains sufficient probability to refute the property under investigation. The effectiveness of this approach is demonstrated by analyzing rare-event properties on a number of biochemical systems.