I investigate formal methods for the modeling and analysis of hybrid and probabilistic systems in the area of medical cyber-physical systems (CPSs), systems and synthetic biology and system design. I'm particularly interested in the development and application of techniques for automated verification, control and synthesis of such systems, which is made challenging by quantitative aspects such as stochastic and continuous non-linear dynamics, as well as the hybrid dynamics that naturally arise in CPSs.

In my current and past research, I have worked on several case studies where providing formal correctness guarantees and correct-by-design model and controller synthesis is critical, including the artificial pancreas for closed-loop diabetes therapy, implantable cardiac devices for treatment of arrhythmias and biological networks for disease prediction and engineering of molecular devices.

Data-driven robust control for insulin therapy
Period: 2016-2017  |  Collaborators: Scott Smolka, Shan Lin, Kin Sum Liu

The artificial pancreas aims to automate treatment of type 1 diabetes (T1D) by integrating insulin pump and glucose sensor through control algorithms. However, fully closed-loop therapy is challenging since the blood glucose levels to control depend on disturbances related to the patient behavior, mainly meals and physical activity.

To handle meal and exercise uncertainties, in our work we construct data-driven models of meal and exercise behavior, and develop a robust model-predictive control (MPC) system able to reject such uncertainties, in this way eliminating the need for meal announcements by the patient. The data-driven models, called uncertainty sets, are built from data so that they cover the underlying (unknown) distribution with prescribed probabilistic guarantees. Then, our robust MPC system computes the insulin therapy that minimizes the worst-case performance with respect to these uncertainty sets, so providing a principled way to deal with uncertainty. State estimation follows a similar principle to MPC and exploits a prediction model to find the most likely state and disturbance estimate given the observations.

We evaluate our design on synthetic scenarios, including high-carbs intake and unexpected meal delays, and on large clusters of virtual patients learned from population-wide survey data sets (CDC NHANES).

Data-driven robust control for insulin therapy
Robust artificial pancreas design

Optimal synthesis of stochastic chemical reaction networks

The automatic derivation of Chemical Reaction Networks (CRNs) with prescribed behavior is one of the holy grails of synthetic biology, allowing for design automation of molecular devices and in the construction of predictive biochemical models.

In this work, we provide the first method for optimal syntax-guided synthesis of stochastic CRNs that is able to derive not just rate parameters but also the structure of the network. Borrowing from the programming language community, we propose a sketching language for CRNs that allows to specify the network as a partial program, using holes and variables to capture unknown components. Under the Linear Noise Approximation of the chemical master equation, a CRN sketch has a semantics in terms of parametric Ordinary Differential Equations (ODEs).

We support rich correctness properties that describe the temporal profile of the network as constraints over mean and variance of chemical species, and their higher order derivatives. In this way, we can synthesize networks where e.g., one of the species exhibit a bell-shape profile or has variance greater than its expectation.

We synthesize CRNs that satisfies the sketch constraints and a correctness specification while minimizing a given cost function (capturing the structural complexity of the network). The optimal synthesis algorithm employs SMT solvers over reals and ODEs (iSAT) and a meta-sketching abstraction that speeds up the search through cost constraints.

We evaluate the approach on a three key problems: synthesis of networks with a bell-shaped profile (occurring in signaling cascades), a CRN implementation of a stochastic process with prescribed levels of noise and synthesis of sigmoidal profiles in the phosphorelay network.

Optimal synthesis of stochastic chemical reaction networks
Top: correctness specification describing the sigmoid/switch-like profile of the final layer in a phosphorelay cascade. The specification requires that the species exhibit an inflection point (at any time). Bottom: species concentrations in the synthesized network.

Precise parameter synthesis for continuous-time Markov chains
Period: 2014-2016  |  Collaborators: Milan Ceska, Marta Kwiatowska, Frits Dannenberg, Peter Pilar, Lubos Brim

Given a parameteric continuous-time Markov chain (pCTMC), we aim at finding parameter values such that a CSL property is guaranteed to hold (threshold synthesis), or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised (max synthesis).

The solution of the threshold synthesis (see picture) is a decomposition of the parameter space into true and false regions that are guaranteed to, respectively, satisfy and violate the property, plus an arbitrarily small undecided region. On the other hand, in the max synthesis problem we identify an arbitrarily small region guaranteed to contain the actual maximum/minimum.

We developed synthesis methods based on a parameteric extension of probabilistic model checking to compute probability bounds, as well as refinement and sampling of the parameter space. We implemented GPU-accelerated algorithms for synthesis in the PRISM-PSY tool, which we applied to a variety of biological and engineered systems, including models of molecular walkers, mammalian cell cycle, and the Google file system.

Precise parameter synthesis for continuous-time Markov chains
Parameter ranges and bounds (vertical axis) for the probability of infection extinction in an epidemic model. Green: true region, i.e., with probability above the desired threshold (transparent plane). Red: false region. Yellow: undecided region.

Probabilistic timed modelling of cardiac dynamics and personalization from ECG

We developed a timed automata translation of the IDHP (Integrated Dual-chamber Heart and Pacer) model by Lian et al. Timed components realize the conduction delays between functional components of the heart and action potential propagation between nodes is implemented through synchronisation between the involved components. In this way, the model can be easily extended with other accessory conduction pathways in order to reproduce specific heart conditions.

The IDHP model can be also parametrised from patient electrocardiogram (ECG) in order to reproduce the specific physiological characteristics of the individual. For this purpose, we extended the model in order to generate synthetic ECG signals that reflect the heart events occurring at simulation time. Starting from raw ECG recordings, our method automatically finds model parameters such that the synthetic signal best mimics the input ECG, by minimising the statistical distance between the two. The resulting parameters correspond to probabilistic delays in order to reflect variability of ECG features.

The IDHP heart model can be downloaded from the tool page, while personalization from ECG data is implemented in the HeartVerify tool.

Probabilistic timed modelling of cardiac dynamics and personalization from ECG
Mean input ECG (red) and mean synthetic ECG (blue) generated from the personalized model.

SMT-based synthesis of gene regulatory networks

Unraveling the structure and the logic of gene regulation is crucial to understand how organisms develop and so is the derivation of predictive models able to reproduce experimental observations and explain unknown biological interactions.

This research centers on the synthesis of biological programs, with specific focus on Boolean gene regulatory networks (GRN). We developed methods based on the idea of synthesis by sketching, which enables explicit modeling of hypotheses and unknown information, specified as e.g. choices or uninterpreted functions. Through the formalization as an SMT problem, the method can automatically and efficiently resolve the unknown information in order to obtain a model that is consistent with observations.

We applied this approach to synthesize the first GRN model of the sea urchin embryo (an important model organism in biology) that precisely and fully reproduce available temporal and spatial expression data and the effects of perturbation experiments. The data we used is the result of 30+ years of research in the Davidson lab at Caltech.

SMT-based synthesis of gene regulatory networks
Synthesis of gene networks. Input: partial gene expression data and uncertain model. Output: synthesized model that reproduces known data and resolves missing data.

Network analysis for bioaccumulation and bioremediation in contaminated food webs

In this project we develop computational methods and models to study pollution dynamics in ecological networks and to shed light on three key questions: How persistent organic pollutants (e.g. PCBs that bind to the fat tissue) are transferred in food webs through feeding connections? What are the species that play role in the pollutant distribution? How to synthesize effective bioremediation strategies mediated by pollutant-degrading bacteria?

We present a computational framework to 1) reconstruct bioaccumulation networks from (partial) data; 2) identify key species in contamination dynamics through a new network index based on sensitivity analysis; and 3) analyze the multiscale effects of microbial bioremediation on species-level contamination by integrating metabolic networks of biodegrading bacteria and bioaccumulation networks.

We consider the case of PCBs bioaccumulation in the Adriatic food web and aerobic PCBs bioremediation by a strain of P. putida (see the Tools page to download the models).

Network analysis for bioaccumulation and bioremediation in contaminated food webs
Circular plot of PCBs bioaccumulation network of the Adriatic ecosystem without bioremediation (top-left), with natural bioremediation acting on detritus and discard (bottom-left) and with in-situ bioremediation acting on water (bottom-right). Ribbons connects predators and prey and have size proportional to the contaminant uptake from food.

Formal analysis of bone remodelling

In this project we study bone remodelling, i.e., the biological process of bone renewal, through the use of computational methods and formal analysis techniques. Bone remodelling is a paradigm for many homeostatic processes in the human body and consists of two highly coordinated phases: resorption of old bone by cells called osteoclasts, and formation of new bone by osteoblasts. Specifically, we aim to understand how diseases caused by the weakening of the bone tissue arise as the resulting process of multiscale effects linking the molecular signalling level (RANK/RANKL/OPG pathway) and the cellular level.

To address crucial spatial aspects such as cell localisation and molecular gradients, we developed a modelling framework based on spatial process algebras and a stochastic agent-based semantics, realised in the Repast Simphony tool. This resulted in the first agent-based model and tool for bone remodelling, see also the Tools page.

In addition, we explored probabilistic model checking methods to precisely assess the probability of a given bone disease to occur, and also hybrid approximations to tame the non-linear dynamics of the system.

Formal analysis of bone remodelling
Screen-shot of the agent-based simulator for bone remodeling. The central panel shows the location of bone cells in the bone remodelling unit. Blue: osteocytes (responsible for signalling that triggers remodelling), green: osteoblasts, red: osteoclasts. On the left side, the graphs for bone density and RANKL concentration. The right panels show bone micro-structure and RANKL diffusion.