Guided search for hybrid systems based on coarse-grained space abstractions.

Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.

STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification.

Extrinsic apoptosis is a programmed cell death triggered by external ligands, such as the TNF-related apoptosis inducing ligand (TRAIL). Depending on the cell line, the specific molecular mechanisms leading to cell death may significantly differ. Precise characterization of these differences is crucial for understanding and exploiting extrinsic apoptosis. Cells show distinct behaviors on several aspects of apoptosis, including (i) the relative order of caspases activation, (ii) the necessity of mitochondria outer membrane permeabilization (MOMP) for effector caspase activation, and (iii) the survival of cell lines overexpressing Bcl2. These differences are attributed to the activation of one of two pathways, leading to classification of cell lines into two groups: type I and type II. In this work we challenge this type I/type II cell line classification. We encode the three aforementioned distinguishing behaviors in a formal language, called signal temporal logic (STL), and use it to extensively test the validity of a previously-proposed model of TRAIL-induced apoptosis with respect to experimental observations made on different cell lines. After having solved a few inconsistencies using STL-guided parameter search, we show that these three criteria do not define consistent cell line classifications in type I or type II, and suggest mutants that are predicted to exhibit ambivalent behaviors. In particular, this finding sheds light on the role of a feedback loop between caspases, and reconciliates two apparently-conflicting views regarding the importance of either upstream or downstream processes for cell-type determination. More generally, our work suggests that these three distinguishing behaviors should be merely considered as type I/II features rather than cell-type defining criteria. On the methodological side, this work illustrates the biological relevance of STL-diagrams, STL population data, and STL-guided parameter search implemented in the tool Breach. Such tools are well-adapted to the ever-increasing availability of heterogeneous knowledge on complex signal transduction pathways.

Robustness analysis and behavior discrimination in enzymatic reaction networks.

Characterizing the behavior and robustness of enzymatic networks with numerous variables and unknown parameter values is a major challenge in biology, especially when some enzymes have counter-intuitive properties or switch-like behavior between activation and inhibition. In this paper, we propose new methodological and tool-supported contributions, based on the intuitive formalism of temporal logic, to express in a rigorous manner arbitrarily complex dynamical properties. Our multi-step analysis allows efficient sampling of the parameter space in order to define feasible regions in which the model exhibits imposed or experimentally observed behaviors. In a first step, an algorithmic methodology involving sensitivity analysis is conducted to determine bifurcation thresholds for a limited number of model parameters or initial conditions. In a second step, this boundary detection is supplemented by a global robustness analysis, based on quasi-Monte Carlo approach that takes into account all model parameters. We apply this method to a well-documented enzymatic reaction network describing collagen proteolysis by matrix metalloproteinase MMP2 and membrane type 1 metalloproteinase (MT1-MMP) in the presence of tissue inhibitor of metalloproteinase TIMP2. For this model, our method provides an extended analysis and quantification of network robustness toward paradoxical TIMP2 switching activity between activation or inhibition of MMP2 production. Further implication of our approach is illustrated by demonstrating and analyzing the possible existence of oscillatory behaviors when considering an extended open configuration of the enzymatic network. Notably, we construct bifurcation diagrams that specify key parameters values controlling the co-existence of stable steady and non-steady oscillatory proteolytic dynamics.

Parameter synthesis in nonlinear dynamical systems: application to systems biology.

The dynamics of biological processes are often modeled as systems of nonlinear ordinary differential equations (ODE). An important feature of nonlinear ODEs is that seemingly minor changes in initial conditions or parameters can lead to radically different behaviors. This is problematic because in general it is never possible to know/measure the precise state of any biological system due to measurement errors. The parameter synthesis problem is to identify sets of parameters (including initial conditions) for which a given system of nonlinear ODEs does not reach a given set of undesirable states. We present an efficient algorithm for solving this problem that combines sensitivity analysis with an efficient search over initial conditions. It scales to high-dimensional models and is exact if the given model is affine. We demonstrate our method on different models of the acute inflammatory response to bacterial infection, and identify initial conditions consistent with three biologically relevant outcomes.