Statistical Model Checking : An Overview <s> Systems Biology <s> The process by which a cell senses and responds to its environment, as in signal transduction, is often mediated by a network of protein-protein interactions, in which proteins combine to form complexes and undergo post-translational modifications, which regulate their enzymatic and binding activities. A typical signaling protein contains multiple sites of protein interaction and modification and may contain catalytic domains. As a result, interactions of signaling proteins have the potential to generate a combinatorially large number of complexes and modified states, and representing signal-transduction networks can be challenging. Representation, in the form of a diagram or model, usually involves a tradeoff between comprehensibility and precision: comprehensible representations tend to be ambiguous or incomplete, whereas precise representations, such as a long list of chemical species and reactions in a network, tend to be incomprehensible. Here, we develop conventions for representing signal-transduction networks that are both comprehensible and precise. Labeled nodes represent components of proteins and their states, and edges represent bonds between components. Binding and enzymatic reactions are described by reaction rules, in which left graphs define the properties of reactants and right graphs define the products that result from transformations of reactants. The reaction rules can be evaluated to derive a mathematical model. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Systems Biology <s> 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. <s> BIB002 </s> Statistical Model Checking : An Overview <s> Systems Biology <s> Rule-based modeling involves the representation of molecules as structured objects and molecular interactions as rules for transforming the attributes of these objects. The approach is notable in that it allows one to systematically incorporate site-specific details about proteinprotein interactions into a model for the dynamics of a signal-transduction system, but the method has other applications as well, such as following the fates of individual carbon atoms in metabolic reactions. The consequences of protein-protein interactions are difficult to specify and track with a conventional modeling approach because of the large number of protein phosphoforms and protein complexes that these interactions potentially generate. Here, we focus on how a rule-based model is specified in the BioNetGen language (BNGL) and how a model specification is analyzed using the BioNetGen software tool. We also discuss new developments in rule-based modeling that should enable the construction and analyses of comprehensive models for signal transduction pathways and similarly large-scale models for other biochemical systems. <s> BIB003
In BIB002 , we considered the verification of complex biological systems. we introduced a new tool, called BioLab, for formally reasoning about the behavior of stochastic dynamic models by integrating SPRT into the BioNetGen BIB001 BIB003 framework for rule-based modeling. We then used BioLab to verify the stochastic bistability of T-cell signalling. There are three more challenges in the systems biology area (the reader is invited to think about these problems and to check the existing literature): 1. How to perform efficient simulations? 2. How to take into account prior knowledge on the model? 3. What are the logics dedicated to biologists than can be model checked with the statistical approach? Remark 7. In fact, statistical model checking techniques recently received a lot of attention in the area of systems biology. As an example, in 2009, Carnegie Mellon University was awarded a 10000000 grant for applying such techniques in the medical area.