Title

Discovering Rare Behaviours In Stochastic Differential Equations Using Decision Procedures: Applications To A Minimal Cell Cycle Model

Keywords

Bioinformatics; Bit-vector; Brownian noise; Cell cycle model; Computational systems biology; Decision procedures; Rare behaviours; Satisfiability modulo theories; SDE; SMT solver; Stochastic differential equation; Stochastic model; Temporal logic

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. Copyright © 2014 Inderscience Enterprises Ltd.

Publication Date

1-1-2014

Publication Title

International Journal of Bioinformatics Research and Applications

Volume

10

Issue

4-5

Number of Pages

540-558

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1504/IJBRA.2014.062999

Socpus ID

84903998748 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/84903998748

This document is currently not available here.

Share

COinS