Automated Reasoning for Systems Biology and Medicine

Formal verification techniques together with other computer science formal methods have been recently tailored for applications to biological and biomedical systems. In contrast to traditional simulation-based approaches, model checking opens an entirely novel way of viewing and analysing the dynamics of such systems. In particular, it can help in system identification and parameter synthesis, in comparison of models with respect to a priori given desired properties, in robustness analysis of systems, in relating models to experimental data, or in globally analysing the bifurcations of systems behaviour with respect to changes in parameters. In this review, we briefly describe the state-of-the-art methods and techniques employing model checking, as one of the most prominent verification techniques, to the analysis of biomedical systems. We demonstrate some of the advantages of using the model checking method by presenting a brief account of the technique itself followed by examples of the application of formal methods based on model checking to three areas related to the analysis of biomedical systems: verification of biological hypotheses, parameters synthesis, and bifurcation analysis. Finally, we discuss several case studies that show how fruitfully the methods can be utilised within the computational systems biology and biomedicine domain.

Cellular decision-making arises as the output of biochemical information processing, as complex cascades of molecular interactions are triggered by input stimuli. Deciphering critical interactions and how they are organised into biological programs is a huge challenge, compounded by the difficulty of manually navigating alternative hypotheses consistent with observed behaviour. Against this backdrop, automated reasoning is a powerful methodology to tackle biological complexity and derive explanations of behaviour that are provably consistent with experimental evidence. We present a reasoning framework that permits the synthesis and analysis of a set of dynamic biological interaction networks. Employing methods based on Satisfiability Modulo Theories (SMT), we encode experimental observations as specifications of expected dynamics, and synthesise networks consistent with these constraints. Predictions of untested behaviour are generated based on all consistent models, without requiring time-consuming simulation or state space exploration, and the method can be used to identify additional components, topological ‘switches’ that allow cell state changes, and to predict gene-level dynamics. We show the reader how to utilise this reasoning framework to encode and explore rich queries for their biological system of choice.

We introduce a framework for analyzing ordinary differential equation  (ODE) models of biological networks using statistical model checking (SMC). A key aspect of our work is the modeling of single-cell variability by assigning a probability distribution to intervals of initial concentration values and kinetic rate constants. We propagate this distribution through the system dynamics to obtain a distribution over the set of trajectories of the ODEs. This in turn opens the door for performing statistical analysis of the ODE system’s behavior. To illustrate this, we first encode quantitative data and qualitative trends as bounded linear time temporal logic (BLTL) formulas. Based on this, we construct a parameter estimation method using an SMC-driven evaluation procedure applied to the stochastic version of the behavior of the ODE system. We then describe how this SMC framework can be generalized to hybrid automata by exploiting the given distribution over the initial states and the—much more sophisticated—system dynamics to associate a Markov chain with the hybrid automaton. We then establish a strong relationship between the behaviors of the hybrid automaton and its associated Markov chain. Consequently, we sample trajectories from the hybrid automaton in a way that mimics the sampling of the trajectories of the Markov chain. This enables us to verify approximately that the Markov chain meets a BLTL specification with high probability. We have applied these methods to ODE-based models of Toll-like receptor signaling and the crosstalk between autophagy and apoptosis, as well as to systems exhibiting hybrid dynamics including the circadian clock pathway and cardiac cell physiology. We present an overview of these applications and summarize the main empirical results. These case studies demonstrate that our methods can be applied in a variety of practical settings.

In this chapter, we present the interplay between models of human physiology, closed-loop medical devices, correctness specifications, and verification algorithms in the context of the artificial pancreas. The artificial pancreas refers to a series of increasingly sophisticated closed-loop medical devices that automate the delivery of insulin to people with type 1 diabetes. On the one hand, they hold the promise of easing the everyday burden of managing type 1 diabetes. On the other hand, they expose the patient to potentially deadly consequences of incorrect insulin delivery that could lead to coma or even death in the short term, or damage to critical organs such as the eyes, kidneys, and the heart in the longer term. Verifying the correctness of these devices involves a careful modeling of human physiology, the medical device, and the surrounding disturbances at the right level of abstraction. We first provide a brief overview of insulin–glucose regulation and the spectrum of associated mathematical models. At one end are physiological models that try to capture the transport, metabolism, uptake, and interactions of insulin and glucose. On the end are data-driven models which include time series models and neural networks. The first part of the chapter examines some of these models in detail in order to provide a basis for verifying medical devices. Next, we present some of the devices which are commonly used in blood glucose control, followed by a specification of key correctness properties and performance measures. Finally, we examine the application of some of the state-of-the-art approaches to verification and falsification of these properties to the models and devices considered. We conclude with a brief presentation on future directions for next generation artificial pancreas and the challenges involved in reasoning about them.

Cancer develops via the progressive accumulation of somatic mutations, which subvert the normal operation of the gene regulatory network of the cell. However, little is known about the order in which mutations are acquired in successful clones. A particular sequence of mutations may confer an early selective advantage to a clone by increasing survival or proliferation, or lead to negative selection by triggering cell death. The space of allowed sequences of mutations is therefore constrained by the gene regulatory network. Here, we introduce a methodology for the systematic exploration of the effect of every possible sequence of oncogenic mutations in a cancer cell modelled as a qualitative network. Our method uses attractor identification using binary decision diagrams and can be applied to both synchronous and asynchronous systems. We demonstrate our method using a recently developed model of ER-negative breast cancer. We show that there are differing levels of constraint in the order of mutations for different combinations of oncogenes, and that the effects of ErbB2/HER2 over-expression depend on the preceding mutations.

The understanding of biological systems and processes requires the development of dynamical models characterized by nonlinear laws and often intricate regulation architectures. Differential and difference equations are common formalisms to characterize such systems. Hybrid dynamical systems come in handy when the modeled system combines continuous and discrete evolutions or different evolution modes such as where slow evolution phases are interrupted by fast ones. Biological data with kinetic content are often scarce, thus it can be appropriate to reason in terms of sets of (parametrized) models and sets of trajectories. In doing so, uncertainties and lack of knowledge are explicitly taken into account and more reliable predictions can be made. A crucial problem in Systems Biology is thus to identify regions of parameter space for which model behavior is consistent with experimental observations. In this chapter, we investigate the use of set-based analysis techniques, designed to compute on sets of behaviors, for the validation of biological models under uncertainties and perturbations. In addition, these techniques can be used for the synthesis of model parameter sets, so that the execution of the considered biological model under the influence of the synthesized parameters is guaranteed to satisfy a given constraint or property. The proposed approach is illustrated by several case studies, namely a model of iron homeostasis in mammalian cells and some epidemic models.

Understanding which are the key components of a system that distinguish a normal from a cancerous cell has been approached widely in the recent years using machine learning and statistical approaches to detect gene signatures and predict cell growth. Recently, the idea of using gene regulatory and signaling networks, in the form of logic programs has been introduced in order to detect the mechanisms that control cells state change. Complementary to this, a large literature deals with constraint-based methods for analyzing genome-scale metabolic networks. One of the major outcome of these methods concern the quantitative prediction of growth rates under both given environmental conditions and the presence or absence of a given set of enzymes which catalyze biochemical reactions. It is of high importance to plug logic regulatory models into metabolic networks by using a gene-enzyme logical interaction rule. In this work, our aim is first to review previously proposed logic programs to discover key components in the graph-based causal models that distinguish different variants of cell types. These variants represent either cancerous versus healthy cell types, multiple cancer cell lines, or patients with different treatment response. With these approaches, we can handle experimental data coming from transcriptomic profiles, gene expression micro-arrays or RNAseq, and (multi-perturbation) phosphoproteomics measurements. In a second part, we deal with the problem of combining both, regulatory and signaling, logic models within metabolic networks. Such a combination allows us to obtain quantitative prediction of tumor cell growth. Our results point to logic program models built for three cancer types: Multiple Myeloma, Acute Myeloid Leukemia, and Breast Cancer. Experimental data for these studies was collected through DREAM challenges and in collaboration with biologists that produced them. The networks were built using several publicly available pathway databases, such as Pathways Interaction Database [39], KEGG [18], Reactome [10], and Trrust [13]. We show how these models allow us to identify the key mechanisms distinguishing a cancerous cell. In complement to this, we sketch a methodology, based on currently available frameworks and datasets, that relates both the linear component of the metabolic networks and the logical part of logic programing-based methods.

The concepts of integrated clinical environments and smart intensive care units refer to complex technological infrastructures where health care relies on interoperating medical devices monitored and coordinated by software applications under human supervision. These complex socio-technical systems have stringent safety requirements that can be met with rigorous and precise development methods. This chapter presents an approach to the formalization of system requirements for integrated clinical environments, using the Prototype Verification System, a theorem-proving environment based on a higher-order logic language. The approach is illustrated by modeling safety-related requirements affecting various aspects of an integrated clinical environment, and in particular the communication network. A simple but realistic wireless communication protocol will be used as an example of computer-assisted verification.

Clinical guidelines are evidence-based care plans which detail the essential steps to be followed when caring for patients with a specific clinical problem, usually a chronic disease (e.g. diabetes, cardiovascular disease, chronic kidney disease, cancer, chronic obstructive pulmonary disease, and so on). Recommendations for chronic diseases include the medications (or group of medications) to be given at different stages of the treatment plan. We present an automated approach which combines constraint solvers and theorem provers to find the best solutions for treatment according to different criteria, and avoiding adverse drug reactions as much as possible. We extended the approach here to further refine the choice(s) to avoid dangerous or undesirable side effects.

The concept of attractor of dynamic biochemical networks has been used to explain cell types and cell alterations in health and disease. We have recently proposed an extension of the notion of attractor to take into account metastable regimes, defined as long-lived dynamical states of the network. These regimes correspond to slow dynamics on low- dimensional invariant manifolds of the biochemical networks. Methods based on tropical geometry allow to compute the metastable regimes and represent them as polyhedra in the space of logarithms of the species concentrations. We are looking for sensitive parameters and tipping points of the networks by analyzing how these polyhedra depend on the model parameters. Using the coupled MAPK and PI3K/Akt signaling networks as an example, we test the idea that large changes of the metastable states can be associated with cancer-specific alterations of the network. In particular, we show that for model parameters representing protein concentrations, the protein differential level between tumors of different types is reasonably reflected in the sensitivity scores, with sensitive parameters corresponding to differential proteins.

Remyelination is a regenerative process that aims to repair damaged regions of the central nervous system, caused by demyelinating diseases, like multiple sclerosis. This process fails to completely repair the demyelinated lesions in many cases and the causes of the failures are not clear. Since many factors and complex mechanisms regulate the process, it is helpful to use high-level modelling languages to describe it and model checking techniques to perform the analysis. They allow us to describe and simulate this stochastic process, and to analyse its behaviour in different scenarios. This study will support neurologists to reason about the different factors that influence this complex process and to create new hypotheses to test through lab experiments. In this chapter, we introduce a novel process algebra called MELA that we used for modelling the remyelination process. We present a number of MELA models capturing different hypotheses about the functioning of remyelination, and their comparison. We perform the analysis of the spatio-temporal evolution of remyelination using Signal Spatio-Temporal Logic and Statistical Model Checking.

There has been an increasing demand for formal methods in the design process of safety-critical synthetic genetic circuits. Probabilistic model checking techniques have demonstrated significant potential in analyzing the intrinsic probabilistic behaviors of complex genetic circuit designs. However, its inability to scale limits its applicability in practice. This chapter addresses the scalability problem by presenting a state-space approximation method to remove unlikely states resulting in a reduced, finite state representation of the infinite-state continuous-time Markov chain that is amenable to probabilistic model checking. The proposed method is evaluated on a design of a genetic toggle switch. Comparisons with another state-of-the-art tool demonstrate both accuracy and efficiency of the presented method.

Intracellular calcium dynamics plays an important role in influencing the outcome of many cellular processes. Constructing and simulating computational models to investigate this biological behaviour are intricate and require the interplay of stochastic and deterministic processes as there are multiple spatial and temporal scales involved. Therefore, many hybrid models have been devised to analyse intracellular calcium dynamics. However, all these models are based on reaction–diffusion equations which are not intuitive for many bioscientists. In contrast, Petri nets do offer an intuitive and graphical approach to model biological processes. To deal with new challenges due to the advances in dynamical modelling, Petri nets have been extended in different directions. Coloured hybrid Petri nets are one of these extensions that support hybrid modelling of complex biological systems using a parametrised language and abstract high-level notations permitting various timing features. In this paper, we present a graphical hybrid model of intracellular calcium dynamics based on coloured hybrid Petri nets. The proposed model can easily be adapted by adjusting a few parameters. Moreover, we illustrate model operations by conducting three simulation experiments in the two-dimensional space. We use Snoopy, a tool to construct and execute qualitative and quantitative Petri nets, to implement the proposed model.

The goal of target-controlled delivery of intravenous (IV) anesthetics is the achievement and maintenance of a suitable depth of hypnosis (DOH) in a fast and safe manner, where DOH is associated with a certain effect site (i.e. brain) drug concentration. Nowadays, the delivery of anesthetic drugs is performed by target-controlled infusion (TCI) pumps adjusting the delivery rate using an algorithm based on pharmacokinetic (PK) models having no feedback. However, the inaccuracy of concentration prediction using this PK model for certain individuals can be up to 100%. In this chapter, we show that the precision of anesthesia delivery can definitely be improved by realising a feedback loop with sensors able to provide measurements of the anesthetic concentration in body fluids in real time. We present two possible approaches for building the control feedback loop using plasma concentration measurements: one representing the classic method in pharmacokinetics based on Bayesian inference and another one being an example of classic method in control theory based on Kalman filter. The first one performs real-time re-estimation of PK model parameters with each new measurement, while the latter one estimates the offset values for drug concentration correction. The adjusted concentration values are further used to compute the personalised delivery rate using the classic TCI algorithm. To validate the algorithms’ robustness, we simulate measurements covering the maximum space of possible values using inter- and intra-patient variability of the statistical Eleveld’s (Eleveld, Proost, Cortinez, Absalom, Struys, Anesth Analg 118(6):1221–1237, 2014, [8]) PK model. This allows one to disturb the system to its extreme before testing it on patients. We provide the robustness analysis of these algorithms with respect to realistic measurement periods and delays.

The decreasing cost of high-throughput technologies allows to consider their use in healthcare and medicine. To prepare for this upcoming revolution, the community is assembling large disease-dedicated datasets such as TCGA or METABRIC. These datasets will serve as references to compare new patient samples to in order to assign them to a predefined category (i.e. ‘patients associated with poor prognosis’). Some problems affecting the downstream analysis remain to be solved, the bottleneck is no longer data generation itself but the integration of the existing datasets with the present knowledge. Constraint-based modelling, that only requires the setting of a few parameters, became popular for the integration of high-throughput data in a metabolic context. Notably, context-specific building algorithms that extract a subnetwork from a reference network are largely used to study metabolic changes in various diseases. Reference networks are composed of canonical pathways while extracted subnetworks include only active pathways in the context of interest based on high-throughput data. Even though these algorithms can be part of automated pipelines, to be applied by clinicians, the model-building pipelines must be coupled to a standardized semi-automated analysis workflow based on machine learning approaches to avoid bias and reduce the cost of diagnostics.

Our capability to engineer biological systems is increasing rapidly in both speed and scale, leading to explosive growth in the complexity of bioengineering projects that can be contemplated. Artificial intelligence techniques have helped to tame such complexity in many other fields, and are beginning to be employed in the same way to the engineering of biological organisms. Using these techniques, computers represent, acquire, and employ domain knowledge to automate “more routine” processes and allow humans to instead focus more on deeper issues of science and engineering. At the same time, applying more sophisticated techniques such as these imposes new demands on biological systems experimentation, particularly with respect to representation and curation of data. This chapter surveys the current state of the art in applying artificial intelligence to bioengineering, as well as discussing opportunities and challenges for the future.

In the recent years, deep learning based methods and, in particular, convolutional neural networks, have been dominating the arena of medical image analysis. This has been made possible both with the advent of new parallel hardware and the development of efficient algorithms. It is expected that future advances in both of these directions will increase this domination. The application of deep learning methods to medical image analysis has been shown to significantly improve the accuracy and efficiency of the diagnoses. In this chapter, we focus on applications of deep learning in microscopy image analysis and digital pathology, in particular. We provide an overview of the state-of-the-art methods in this area and exemplify some of the main techniques. Finally, we discuss some open challenges and avenues for future work.