Computer Science Department
School of Computer Science, Carnegie Mellon University


Statistical Model Checking for Complex
Stochastic Models in Systems Biology

Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead,
Axel Legay, André Platzer, Paolo Zuliani

April 2009


Keywords: Model checking, temporal logic, stochastic systems, statistical hypothesis testing, systems biology, biochemical pathways, parameter synthesis

Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than state-of-the-art techniques, even when no prior knowledge is available.

47 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by