This report proposes a novel framework for a rigorous robustness analysis of stochastic biochemical systems. The technique is based on probabilistic model checking. We adapt the general definition of robustness introduced by Kitano to the class of stochastic systems modelled as continuous time Markov Chains in order to extensively analyse and compare robustness of biological models with uncertain parameters. The framework utilises novel computational methods that enable to effectively evaluate the robustness of models with respect to quantitative temporal properties and parameters such as reaction rate constants and initial conditions. The framework is applied to gene regulation as an example of a central biological mechanism where intrinsic and extrinsic stochasticity plays crucial role due to low numbers of DNA and RNA molecules. Using our methods we have obtained a comprehensive and precise analysis of stochastic dynamics under parameter uncertainty. Furthermore, we apply our framework to compare several variants of two-component signalling networks from the perspective of robustness with respect to intrinsic noise caused by low populations of signalling components. We succeeded to extend previous studies performed on deterministic models (ODE) and show that stochasticity may significantly affect obtained predictions. Our case studies demonstrate that the framework can provide deeper insight into the role of key parameters in maintaining the system functionality and thus it significantly contributes to formal methods in computational systems biology.
@cite_30: The newly emerging field of computational cell biology requires software tools that address the needs of a broad community of scientists. Cell biological processes are controlled by an interacting set of biochemical and electrophysiological events that are distributed within complex cellular structures. Computational modeling is familiar to researchers in fields such as molecular structure, neurobiology and metabolic pathway engineering, and is rapidly emerging in the area of gene expression. Although some of these established modeling approaches can be adapted to address problems of interest to cell biologists, relatively few software development efforts have been directed at the field as a whole. The Virtual Cell is a computational environment designed for cell biologists as well as for mathematical biologists and bioengineers. It serves to aid the construction of cell biological models and the generation of simulations from them. The system enables the formulation of both compartmental and spatial models, the latter with either idealized or experimentally derived geometries of one, two or three dimensions.
@cite_22: An important problem in current computational systems biology is to analyze models of biological systems dynamics under parameter uncertainty. This paper presents a novel algorithm for parameter synthesis based on parallel model checking. The algorithm is conceptually universal with respect to the modeling approach employed. We introduce the algorithm, show its scalability, and examine its applicability on several biological models.
@cite_7: Recent progress in high-throughput data-production technologies pushes research toward systems biology, focusing on the global interaction between the components of biomolecular processes. In this article we present a formal modelling environment for network biology, called the Biochemical Abstract Machine (BIOCHAM). Biocham delivers precise semantics to biomolecular interaction maps. Based on this formal semantics, the Biocham system offers automated reasoning tools for querying the temporal properties of the system under all its possible behaviours. We present the main features of Biocham and report on our modelling experience with this language
@cite_32: We describe Breach, a Matlab C++ toolbox providing a coherent set of simulation-based techniques aimed at the analysis of deterministic models of hybrid dynamical systems The primary feature of Breach is to facilitate the computation and the property investigation of large sets of trajectories It relies on an efficient numerical solver of ordinary differential equations that can also provide information about sensitivity with respect to parameters variation The latter is used to perform approximate reachability analysis and parameter synthesis A major novel feature is the robust monitoring of metric interval temporal logic (MITL) formulas The application domain of Breach ranges from embedded systems design to the analysis of complex non-linear models from systems biology.
@cite_40: In this paper, we consider the robust interpretation of Metric Temporal Logic (MTL) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, @e, from unsatisfiability. We prove that any other signal that remains @e-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely Metric Interval Temporal Logic (MITL) and closed Metric Temporal Logic (clMTL), over continuous-time signals using only discrete-time analysis. The motivating idea behind our approach is that if the continuous-time signal fulfills certain conditions and the discrete-time signal robustly satisfies the temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification.
@cite_20: Motivation: Simulation and modeling is becoming a standard approach to understand complex biochemical processes. Therefore, there is a big need for software tools that allow access to diverse simulation and modeling methods as well as support for the usage of these methods. Results: Here, we present COPASI, a platform-independent and user-friendly biochemical simulator that offers several unique features. We discuss numerical issues with these features; in particular, the criteria to switch between stochastic and deterministic simulation methods, hybrid deterministic--stochastic methods, and the importance of random number generator numerical resolution in stochastic simulation. Availability: The complete software is available in binary (executable) for MS Windows, OS X, Linux (Intel) and Sun Solaris (SPARC), as well as the full source code under an open source license from http: www.copasi.org. Contact: mendes@vbi.vt.edu
@cite_10: We consider temporal logic formulae specifying constraints in continuous time and space on the behaviors of continuous and hybrid dynamical system admitting uncertain parameters. We present several variants of robustness measures that indicate how far a given trajectory stands, in space and time, from satisfying or violating a property. We present a method to compute these robustness measures as well as their sensitivity to the parameters of the system or parameters appearing in the formula. Combined with an appropriate strategy for exploring the parameter space, this technique can be used to guide simulation-based verification of complex nonlinear and hybrid systems against temporal properties. Our methodology can be used for other non-traditional applications of temporal logic such as characterizing subsets of the parameter space for which a system is guaranteed to satisfy a formula with a desired robustness degree.
@cite_12: 
In the domain of ODE models, there exist several analytic methods for effective analysis under parameter uncertainty. They build on static analysis (stoichiometric analysis, flux balance analysis) as well as dynamic numerical methods (simulation, monitoring by temporal formulae, sensitivity analysis) implemented in tools (e.g. @cite_20 @cite_30 @cite_7 ). Robustness analysis with respect to functionality specified in terms of temporal formulae has been introduced recently @cite_40 @cite_12 . There exist two major approaches how to define and analyse robustness. If only parameters of the model are perturbed, we speak of a to robustness. This approach has been explored by Fainekos & Pappas @cite_40 , further extended by A. Donz ' e et al @cite_10 and implemented in the toolbox Breach @cite_32 . Another option could be to perturb the model structure i.e. the reaction topology, as this is done in many gene knock-out biological experiments. Such changes are in principle discrete and the problem of robustness computation for such perturbations would reduce to solving many individual instances of the same problem for each discrete topology. However identifying model behaviour shared among individual perturbations can lead to more efficient analysis @cite_22 .