Title

Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement

Authors

Authors

S. K. Jha;C. J. Langmead

Comments

Authors: contact us about adding a copy of your work at STARS@ucf.edu

Abbreviated Journal Title

Theor. Comput. Sci.

Keywords

Systems biology; Stochastic systems; Parameter synthesis; Model; infeasibility; Statistical model checking; LINEAR HYBRID AUTOMATA; SYMBOLIC REACHABILITY ANALYSIS; PARAMETER; SYNTHESIS; SENSITIVITY-ANALYSIS; BIOLOGICAL-SYSTEMS; TEMPORAL LOGIC; SIMULATION; NETWORKS; COMPUTATION; Computer Science, Theory & Methods

Abstract

The stochastic dynamics of biochemical reaction networks can be modeled using a number of succinct formalisms all of whose semantics are expressed as Continuous Time Markov Chains (CTMC). While some kinetic parameters for such models can be measured experimentally, most are estimated by either fitting to experimental data or by performing ad hoc, and often manual search procedures. We consider an alternative strategy to the problem, and introduce algorithms for automatically synthesizing the set of all kinetic parameters such that the model satisfies a given high-level behavioral specification. Our algorithms, which integrate statistical model checking and abstraction refinement, can also report the infeasibility of the model if no such combination of parameters exists. Behavioral specifications can be given in any finitely monitorable logic for stochastic systems, including the probabilistic and bounded fragments of linear and metric temporal logics. The correctness of our algorithms is established using a novel combination of arguments based on survey sampling and uniform continuity. We prove that the probability of a measurable set of paths is uniformly and jointly continuous with respect to the kinetic parameters. Under a suitable technical condition, we also show that the unbiased statistical estimator for the probability of a measurable set of paths is monotonic in the parameter space. We apply our algorithms to two benchmark models of biochemical signaling, and demonstrate that they can efficiently find parameter regimes satisfying a given high-level behavioral specification. In particular, we show that our algorithms can synthesize up to 6 parameters, simultaneously, which is more than that reported by any other synthesis algorithm for stochastic systems. Moreover, when parameter estimation is desired, as opposed to synthesis, we show that our approach can scale to even higher dimensional spaces, by identifying the single parameter combination that maximizes the probability of the behavior being true in an 11-dimensional system. (C) 2011 Elsevier BM. All rights reserved.

Journal Title

Theoretical Computer Science

Volume

412

Issue/Number

21

Publication Date

1-1-2011

Document Type

Article

Language

English

First Page

2162

Last Page

2187

WOS Identifier

WOS:000290078000007

ISSN

0304-3975

Share

COinS