title: Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model.
abstract: Stochastic Differential Equation (SDE) models are used to describe the dynamics of complex systems with inherent randomness. The primary purpose of these models is to study rare but interesting or important behaviours, such as the formation of a tumour. Stochastic simulations are the most common means for estimating (or bounding) the probability of rare behaviours, but the cost of simulations increases with the rarity of events. To address this problem, we introduce a new algorithm specifically designed to quantify the likelihood of rare behaviours in SDE models. Our approach relies on temporal logics for specifying rare behaviours of interest, and on the ability of bit-vector decision procedures to reason exhaustively about fixed-precision arithmetic. We apply our algorithm to a minimal parameterised model of the cell cycle, and take Brownian noise into account while investigating the likelihood of irregularities in cell size and time between cell divisions.
authors.affiliation: Computer Science Department, University of Central Florida, Orlando FL 32816, USA.
authors.forename: Arup Kumar
authors.initials: AK
authors.lastname: Ghosh
authors.affiliation: Computer Science Department, University of Central Florida, Orlando FL 32816, USA.
authors.forename: Faraz
authors.initials: F
authors.lastname: Hussain
authors.affiliation: Strategic CAD Labs, Intel, Portland, OR 97124, USA.
authors.forename: Susmit
authors.initials: S
authors.lastname: Jha
authors.affiliation: Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA; Lane Center for Computational Biology, Carnegie Mellon University, Pittsburgh PA 15213, USA.
authors.forename: Christopher J
authors.initials: CJ
authors.lastname: Langmead
authors.affiliation: Computer Science Department, University of Central Florida, Orlando FL 32816, USA.
authors.forename: Sumit Kumar
authors.initials: SK
authors.lastname: Jha
mesh_terms: D000465:Algorithms; D002453:Cell Cycle; D048429:Cell Size; D019295:Computational Biology / Q000379:methods*; D003657:Decision Making; D008954:Models, Biological; D015233:Models, Statistical; D011336:Probability; D012984:Software; D013269:Stochastic Processes; D013997:Time Factors
keywords: Brownian noise; SDE; SMT solver; bioinformatics; bit–vector; cell cycle model; cell divisions; cell size; computational systems biology; decision procedures; rare behaviours; satisfiability modulo theories; stochastic differential equation; stochastic modelling; temporal logic