2008 | OriginalPaper | Chapter
Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway
Authors : Edmund M. Clarke, James R. Faeder, Christopher J. Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay
Published in: Computational Methods in Systems Biology
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present an algorithm, called
BioLab
, for verifying temporal properties of rule-based models of cellular signalling networks.
BioLab
models are encoded in the
BioNetGen
language, and properties are expressed as formulae in probabilistic bounded linear temporal logic. Temporal logic is a formalism for representing and reasoning about propositions qualified in terms of time. Properties are then verified using sequential hypothesis testing on executions generated using stochastic simulation.
BioLab
is optimal, in the sense that it generates the minimum number of executions necessary to verify the given property.
BioLab
also provides guarantees on the probability of it generating Type-I (i.e., false-positive) and Type-II (i.e., false-negative) errors. Moreover, these error bounds are pre-specified by the user. We demonstrate
BioLab
by verifying stochastic effects and bistability in the dynamics of the T-cell receptor signaling network.