Safety Analysis of Sugar Cataract Development Using Stochastic Hybrid Systems

摘要

Modeling and analysis of biochemical systems are important tasks because they can unlock insights into the complicated dynamics of systems which are difficult or expensive to test experimentally. A variety of techniques have been used to model biochemical systems, but the effectiveness of the analysis techniques is often limited by tradeoffs imposed by the modeling paradigms. Stochastic differential equations have been used to model biochemical reactions [5,2]; however, analysis of these models has mainly been limited to simulation. Hybrid systems have also been used to model biochemical systems [4]; however, verification methods based on deterministic hybrid systems fail to capture the probabilistic nature of some biochemical processes and therefore may not be able to correctly analyze certain systems. Stochastic Hybrid Systems (SHS) have been used to capture the stochastic nature of biochemical systems but have previously only been used for simulations [10] or analysis of systems with simplified continuous dynamics [6].rnIn this paper we model Sugar Cataract Development (SCD) as a SHS, and we present a probabilistic verification method for computing the probability of sugar cataract formation for different chemical concentrations. An accumulation of sorbitol in the eye is theorized to be the main factor in the SCD process. Un-derstanding the exact conditions that lead to the development of sugar cataracts will help scientists better predict and prevent the condition [2]. The chemical reactions and kinetic constants for the system have been previously studied [8].The stochastic dynamics for biochemical processes can be accurately modeled by the chemical master equation which, however, is impossible to solve for most practical systems [5]. The Stochastic Simulation Algorithm (SSA) is equivalent to solving the master equation based on a discrete model by simulating one reaction at a time, but if the number of molecules of any of the reactants is large, the SSA is not efficient [10]. For verification, it is computationally in-tractable to enumerate all possible states of the model employed by the SSA. Our approach suggests starting with the continuous stochastic dynamics and generating discrete approximations with coarser (and variable) resolution unlike the fixed, overly-fine resolution of the SSA. The discrete approximations can then be used for verification of reachability properties [7].