6th Workshop on Hybrid Systems & BiologyHSB 2019

The understanding of mechanisms that control epigenetic changes is an important research area in modern functional biology. Epigenetic modifications such as DNA methylation are in general very stable over many cell divisions. DNA methylation can however be subject to specific and fast changes over a short time scale even in non dividing (i.e. not-replicating) cells. Such dynamic DNA methylation changes are caused by a combination of active demethylation and de novo methylation processes which have not been investigated in integrated models. Here we present a hybrid (hidden) Markov model to describe the cycle of methylation and demethylation over (short) time scales. Our hybrid model describes several molecular events either happening at deterministic points (i.e. describing mechanisms that occur only during cell division) and other events occurring at random time points. We test our model on mouse embryonic stem cells using time-resolved data. We predict methylation changes and estimate the efficiencies of the different modification steps related to DNA methylation and demethylation.

Charalampos Kyriakopoulos

Saarland University

Pascal Giehr

Saarland University

Alexander Lück

Saarland University

Jörn Walter

Saarland University

Verena Wolf

Saarland University

Germany

Protein levels can be controlled by regulating protein synthesis or half life. The aim of this paper is to investigate how introducing feedback in burst frequency or protein decay rate affects the stochastic distribution of protein level. Using a tractable hybrid mathematical framework, we show that the two feedback pathways lead to the same mean and noise predictions in the small-noise regime. Away from the small-noise regime, feedback in decay rate outperforms feedback in burst frequency in terms of noise control. The difference is particularly conspicuous in the strong-feedback regime. We also formulate a fine-grained discrete model which reduces to the hybrid model in the large system-size limit. We show how to approximate the discrete protein copy-number distribution and its Fano factor using hybrid theory. We also demonstrate that the hybrid model reduces to an ordinary differential equation in the limit of small noise. Our study thus contains a comparative evaluation of feedback in burst frequency and decay rate, and provides additional results on model reduction and approximation.

Pavol Bokes

Comenius University

Abhyudai Singh

University of Delaware

United States

Stochastic population models are widely used to model phenomena in different areas such as chemical kinetics or collective animal behaviour. Quantitative analysis of stochastic population protocols easily becomes challenging, due to the combinatorial propagation of dependencies across the population. The complexity becomes especially prominent when model’s parameters are not known and available measurements are limited. In this paper, we illustrate this challenge on a concrete scenario: we assume a simple communication scheme among identical individuals, inspired by how social honeybees emit the alarm pheromone to protect the colony in case of danger. Together, n individuals induce a population Markov chain model with n parameters. In addition, we assume to be able to experimentally observe the states only after the steady-state is reached. In order to obtain the parameters of the individual’s behaviour, by utilising the available data, and without making any further modelling assumption, we combine two existing techniques. First, we use the tools for parameter synthesis for Markov chains with respect to temporal logic properties, and then we employ CEGAR-like reasoning to find the viable parameter space up to desired coverage. We report the performance on a number of synthetic data sets.

Matej Hajnal

Masaryk University

Tatjana Petrov

Universität Konstanz

Germany

David Safranek

Masaryk University

Czech Republic

Morgane Nouvian

University of Konstanz

Cell signaling plays an important role in the normal functioning of cells and in health conditions such as cancers and immune diseases. Cell signaling models, capturing the transformations of many different molecular species, are one of the most successful applications of dynamical systems biology. Since they involve highly nonlinear dynamics, the predicting power of these models is often limited due to the difficulty in estimating the relevant kinetic parameters. Fluorescent labeling in conjunction with super-resolution microscopy provides in vivo trajectories of receptors and other bio-molecules of interest. This modality is possibly the most direct source of quantitative information on molecular processes in cells. Unfortunately, it is separated by a few orders of magnitude from the resolution of current quantitative models of cell signaling. Signaling models typically require properties (concentrations, reaction rates) averaged over the entire cell; single particle tracking looks at individual molecules in small fraction of the cell. In principle, the gap in resolution can be bridged using simulations: validate a fully spatial model at SPT resolution, then use a consistent abstraction / averaging procedure to infer effective kinetics on larger spatial scales. Extrapolating diffusion coefficients and dimerization rates observed at SPT resolution is complicated by the presence of spatial structure that interferes with the free movement of molecules of interest. Here we present a method used to identify such structures, based on deviations from ideal Brownian motion and outline a framework aimed at refinement using simulated motion in a known landscape.

Ádám Halász

West Virginia University

United States

Ouri Maler

West Virginia University

Jeremy S Edwards

University of New Mexico

The analysis of equilibria of ordinary differential equations (ODEs) that represent biochemical reaction networks is crucial in order to understand various functional properties of regulation in systems biology. In this paper, we develop a numerical algorithm to compute equilibria under the assumption that the regulatory network satisfies certain graph-theoretic conditions which lead to fixed-point iterations over an anti-monotonic function. Unlike generic approaches based on Newton’s method, our algorithm does not require the availability of the Jacobian of the ODE vector field, which may be expensive when the dimensionality of the system is large. More important, it produces an estimation (through over-approximation) of the entire set of equilibria, with the guarantee of yielding the unique equilibrium of the ODE in the case that the returned set is a singleton. We demonstrate the applicability of our algorithm to two signaling pathways of MAPK and EGFR.

Isabel Cristina Perez-Verona

IMT Institute for Advanced Studies Lucca, Italy

Mirco Tribastone

IMT Institute for Advanced Studies Lucca, Italy

Max Tschaikowski

IMT Institute for Advanced Studies Lucca, Italy

Oded Maler often characterized as “barbaric” some of his approaches to solving complex problems. By this, he meant the modern meaning, i.e., “unsophisticated”, for example when he suggested to compute bunch of simulations to approximate reachable sets of dynamical systems - at a time when the trend was to fill pages of fancy theorems in advanced computational geometry or functional analysis. However, it is fair to say that he was in effect a true Barbarian but in the antique sense: Ancient Greeks called “Barbarians” those who were not Greek themselves. As a matter of fact, Oded as a scientist knew no boundaries: he wandered freely between theoretical computer science and applied mathematics, control theory, logics, Physics and Biology, etc. Always with humility, humor, and avid curiosity about local customs and knowledge he would bring in his own extended scientific baggage with genuine intention and efforts to mix in and contribute to the fields he was exploring. Systems Biology was a natural target of these explorations. There he found problems related to hybrid dynamical systems, another cross-field he contributed to pioneer. Together with various collaborators including biologists, both from wet labs and theoreticians, and myself, we experimented with and improved techniques such as systematic simulation and the monitoring of signal temporal logic, an extension of a logic used in program verification adapted to continuous and real-world processes, to help in particular with the difficult problem of parameter uncertainty in the modeling of living systems. I will try to recount some results we obtained and the avenues of research that this work from Oded’s legacy helped create and remain open today.

Alexandre Donze

University of California, Berkeley

Symbolic systems biology aims to explore biological processes as whole systems instead of small and independent elements. The goal is to define formal models that capture biologists intuitions and reasoning. Pathway Logic is a system for developing executable formal models of biomolecular processes. Using the Maude system, these models of dynamic processes can be represented and analyzed. The Pathway Logic Assistant uses forwards and backwards collection to assemble a connected set of rules from a rule knowledge base to model a system specified by an initial state (experimental setup). For this to succeed the rules must represent component states at the same level of detail, while we would like the knowledge base to capture as much detail as possible. In this paper, we propose a different way to perform matching in the process of rewriting in the high-performance rewriting language Maude. The basic concept is that of ‘‘fuzzy match’’ or ‘‘fuzzy instantiates to’’. It will be used to check requirements imposed by controls in forward collection, and with some elaboration to check whether the change part of a rule applies forwards or backwards.

Adrian Riesco

Universidad Complutense de Madrid

Spain

Beatriz Santos-Buitrago

Seoul National University

Merrill Knapp

SRI International

Gustavo Santos-Garcia

Universidad de Salamanca

Carolyn Talcott

SRI International

Fluid approximations have been greatly successful in approximating the macro-scale behaviour of Markov systems with a large number of discrete states. However, these methods rely on the continuous-time Markov chain (CTMC) having a particular population structure which suggests a natural continuous state-space endowed with a dynamics for the approximating process.

We construct here a general method based on spectral analysis of the transition matrix of the CTMC, without the need for a population structure. Specifically, we use the popular manifold learning method of diffusion maps to analyse the transition matrix as the operator of a hidden continuous process. An embedding of states in a continuous space is recovered, and the space is endowed with a drift vector field inferred via Gaussian process regression. In this manner, we construct an ODE whose solution approximates the evolution of the CTMC mean, mapped onto the continuous space (known as the fluid limit).

Michalis Michaelides

University of Edinburgh

Jane Hillston

University of Edinburgh

United Kingdom

Guido Sanguinetti

University of Edinburgh

United Kingdom

Starting from the 20s, researchers have begun to explore the possibility to create ‘hybrid’ systems in vitro at the interface between neuroscience and robotics (I will call them ‘neurohybrid interfaces’), thus providing an excellent test bed for modulation of neuronal tissue and forming the basis of future adaptive, bi-directional Brain Machine Interfaces and neuroprostheses. The first-ever in vitro closed-loop neurohybrid system consisted of a lamprey brainstem bi-directionally connected to a small wheeled robot. Inspired by that and other pioneering studies, a bi-directional system involving in vitro neocortical networks grown on Micro Electrode Arrays (MEAs) and a small robot was developed and tested in my lab. A similar technology could be exploited also for brain repair, with relevance in the field of cognitive neuroprosthetics. The idea is to use closed-loop neurohybrid interfaces to treat the neuronal injury in the brain, where the damage is actually located, and to possibly promote brain plasticity in order to speed up the recovery process. Within this framework, I will show two examples. I will start by presenting the development and the results related to an in vitro ‘brain-prosthesis’, aimed at restoring the communications between damaged neuronal networks. Then, I will present recent results related to closed-loop paradigms for brain repair in vivo, focusing on how different types of stimulation can affect the neural activity. Further developments and applications in the fields of neurorehabilitation and neurorobotics will be briefly introduced and discussed.

Michela Chiappalone

Italian Institute of Technology

Italy

The prevalence of wearable sensing devices and smartphones is resulting in a multitude of physiological data being collected, for example heart rate, gait and eye movement. Driven by applications in health and behavioural monitoring, as well as affective computing, there is a growing demand for computational models that are able to accurately predict multimodal features in a variety of contexts. While machine learning models excel at identifying features in physiological signals, they lack reliability guarantees and need to be adapted to the user. This talk will give an overview of modelling and personalisation techniques developed as part of the AffecTech project (http://www.cs.ox.ac.uk/projects/AFFECTech/index.html) and their applications in the context of biometric security and emotion recognition. Future challenges in this important field will also be discussed.

Marta Kwiatkowska

University of Oxford

Reaction network theories are tools for stability analysis of open reacting systems provided that stoichiometric (chemical) equations are given for each reaction step together with power law rate expressions. Based on stoichiometry alone, elementary subnetworks (known also as elementary modes or extreme currents) are identified and their capacity for displaying dynamical instabilities, such as bistability and oscillations, is evaluated by examining associated Jacobian matrix. This analysis is qualitative in the sense that only reaction orders are needed as input information, whereas rate coefficients may remain unspecified. In the next step, the subnetworks are combined to form the entire network and its stability is determined by stability of the constituting subnetworks. This combination principle can be conveniently used for kinetic parameter estimation of the unknown/unspecified rate coefficients by applying linear optimization to a set of constraint equations balancing linearly combined subnetworks with the corresponding rate expressions. Mathematically, this amounts to convex optimization. From the application point of view, we wish to describe an experimentally measured biosystem in which chemical processes take place (such as enzyme control loops, metabolism, gene regulation, etc.) giving rise to experimentally observed change from a steady state to oscillatory or bistable dynamics. For such a system a reaction mechanism is assumed (or available from previous research) with only a limited set of known kinetic parameters, in addition to input/output parameters known from the experiment. Then the set of unknown kinetic parameters is estimated via linear optimization so that the dynamics displayed by the model coincides with the experimentally observed behavior (emergence of oscillations or bistable switch). Such an estimate may not yield the ultimate best fit, rather, it helps to locate a region in the parameter space, where the observed dynamics are reproduced by the model. This global approach is useful especially when the number of unknown parameters is large. Once a suitable parameter region is found, standard least-square methods or other more refined algorithms assuming a well chosen initial guess may be used to fine tune the parameters values. In addition, reaction network theory is useful in identifying subnetworks that are responsible for destabilizing the steady state. In particular, such subnetworks provide prototypes of chemical oscillators, also called oscillatory motifs, which possess a characteristic network topology. Thus the search for dynamical instabilities in arbitrarily large networks, as is typical in biosystems, can be reduced to the search for motifs.

Igor Schreiber

University of Chemistry and Technology of Prague

Oded Maler was one of the founders of the workshop Hybrid Systems Biology. His contributions in this domain could be traced back to his young days as a curious and brave computer scientist trying to break into Control Sciences, a neighbouring land yet full of distinct customs and traditions. This ambitious venture fruitfully impacted the evolution of the two domains. His results enlarged the theoretical boundary of his Computer Science homeland by extending timed systems to hybrid systems, addressing the fundamental decidability and complexity questions, laying the foundations for formal verification and synthesis of hybrid systems. Furthermore, these results have major intellectual impacts on the control community who began to embrace formal methods.

Being constantly attentive to other disciplines, Oded continued his journey and was particularly interested in systems biology (among others, such as embedded system scheduling and implementation, analog and mixed-signal circuits). His major contribution is his adaptation and proliferation of temporal logics, algorithmic analysis, and more generally hybrid computational thinking to this domain.

In this presentation, I will talk only about some of Oded’s influential contributions in hybrid systems along this remarkable odyssey.

Thao Dang

CNRS/VERIMAG

France

Comprehensive Modelling Platform is a general framework for public sharing, annotation, and visualisation of domain-specific biological models. For a selected system (e.g. an organism, particular process), the framework is instantiated as a web-based application which allows capturing several aspects of biological models represented as biochemical reaction networks or ordinary differential equations.

Matej Troják

Masaryk University

David Safranek

Masaryk University

Czech Republic

Jan Červený

Global Change Research Institute CAS

Marek Havlík

Masaryk University

Lukrécia Mertová

Masaryk University

Matej Hajnal

Masaryk University

Jakub Hrabec

Masaryk University

Jakub Šalagovič

Masaryk University

We introduce a metabolic-regulatory network model (MRN) extending the self-replicator system proposed by Molenaar et al. (2011). Our model allows integrating metabolism with catalytic macromolecules, structural building blocks and regulatory proteins. Using MRN, we show that the dynamic interplay between cellular metabolism, macromolecule production and regulation can be formalized by a hybrid automaton, combining continuous dynamics and discrete control.

Lin Liu

Freie Universität Berlin

Alexander Bockmayr

Freie Universität Berlin

Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive.

Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better while being statistically equivalent.

Gerrit Großmann

Saarland University

Verena Wolf

Saarland University

Germany

Synthesis methods based on formal reasoning are a powerful way to automate the process of constructing computational models of gene regulatory networks (GRNs) and increase predictive power by considering a set of consistent models that are guaranteed to satisfy known experimental data. Previously, a formal reasoning based approach enabling the synthesis and analysis of biological networks formalized using Abstract Boolean Networks (ABNs) was developed, where the precise interactions and update rules are only partially known. System dynamics can be constrained with specifications of some required behaviors, thereby providing a characterization of the set of all networks capable of reproducing given experimental observations. The synthesis method is supported by a tool, the Reasoning Engine for Interaction Networks (RE:IN). Starting with the synthesis framework supported by RE:IN, we provide translations of experimental observations to temporal logic and semantics of Abstract Boolean Networks, enabling us to use off-the-shelf model checking tools and algorithms. An initial prototype implementation we have developed demonstrates this is a gainful approach, providing speed-up gains for some benchmarks, while also opening the way to study extensions of the experimental observations specification language currently supported in RE:IN by using the rich expressive power of temporal logic.

Judah Goldfeder

Yeshiva University

Hillel Kugler

Microsoft

United States

At timed level of abstraction, system behaviors are considered as sequences of discrete events (from a finite alphabet) and real-valued time lapses between them; or as discrete-valued signals over continuous time. Initiated by works of Alur & Dill and aiming modeling and verification of real-time sequences, this approach became quite popular was successfully extended to other domains. As usual in verification, sets of timed behaviors were defined by (timed) automata, and by logical formulas.

In mid 90s, Oded Maler initiated a search for simpler, suitable for engineers, and still powerful formalism to describe sets of timed behaviors. After overcoming many technical obstacles, timed regular expressions were born, and their equivalence to timed automata proven. In follow-up works, alternative formalisms have been proposed by several researchers.

In 2010s, Oded Maler and his group came back to timed regular expressions, with a new optics of pattern-matching: given a (large) record of timed behavior of a system, and a timed regular expression describing patterns of interest (e.g. faulty sequences), detect all the occurrences of the pattern in the record. Most of this research is automata-free: pattern-matching algorithms work directly on timed behaviors. Efficient algorithms have been developed and implemented, allowing off-line and on-line pattern-matching, and using several formalisms for pattern specification, and applications to monitoring prospected.

In this talk I will present the timed view on system behaviors, and the two periods of timed regular expressions: theoretical study on expressiveness from 1990s and practice-oriented works on pattern-matching and monitoring from 2010s. No special knowledge is required from the audience. This will also be a memorial talk, on Oded’s philosophical, creative and personal style of choosing research topics, leading research, and supervising students and co-workers.

Eugene Asarin

IRIF, University Paris Diderot and CNRS, France

Metabolism and cell cycle are two central processes in the life of a eukaryote cell. If they have been extensively studied in their own right, their interconnection remains relatively poorly understood. In this paper, we propose to use a differential model of the central carbon metabolism. After verifying it reproduces major known variations across the cell cycle’s phases, we extend it into a hybrid system reproducing an imposed succession of the phases. This first hybrid approach recovers interesting dynamical results, providing a good first step towards a more complex hybrid system.

Cecile Moulin

Laboratoire de Recherche en Informatique, Université Paris-Saclay & UMR CNRS 8623

Laurent Tournier

MaIAGE, INRA, Université Paris-Saclay.

Sabine Peres

Laboratoire de Recherche en Informatique, Université Paris-Saclay & UMR CNRS 8623.

In this work we introduce the software rPrism, as an branch of the software PRISM model checker, in order to be able to study weighted reactive state transition models. This kind of model gathers together the concepts of reactivity - which consists on the capacity of a state transition model to alter its accessibility relation - and weights, which can be seen as costs, rates, etc.. Given a specific model, the tool performs a simulation based on a Continuous Time Markov Chain. In particular, we show an example of its application for biological systems.

Daniel Figueiredo

University of Aveiro

Eugénio A. M. Rocha

University of Aveiro

Madalena Chaves

INRIA

Manuel A. Martins

University of Aveiro