Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data

Stochastic population models are widely used to model phenomena in different areas such as cyber-physical systems, chemical kinetics, collective animal behaviour, and beyond. Quantitative analysis of stochastic population models easily becomes challenging due to the combinatorial number of possible states of the population. Moreover, while the modeller easily hypothesises the mechanistic aspects of the model, the quantitative parameters associated to these mechanistic transitions are difficult or impossible to measure directly. In this paper, we investigate how formal verification methods can aid parameter inference for population discrete-time Markov chains in a scenario where only a limited sample of population-level data measurements-sample distributions among terminal states-are available. We first discuss the parameter identifiability and uncertainty quantification in this setup, as well as how the existing techniques of formal parameter synthesis and Bayesian inference apply. Then, we propose and implement four different methods, three of which incorporate formal parameter synthesis as a pre-computation step. We empirically evaluate the performance of the proposed methods over four representative case studies. We find that our proposed methods incorporating formal parameter synthesis as a pre-computation step allow us to significantly enhance the accuracy, precision, and scalability of inference. Specifically, in the case of unidentifiable parameters, we accurately capture the subspace of parameters which is data-compliant at a desired confidence level.

Boolean Network Sketches: A Unifying Framework for Logical Model Inference

MOTIVATION

The problem of model inference is of fundamental importance to systems biology. Logical models (e.g., Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only.

RESULTS

We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network's topology and the update logic (obtained through, e.g., a biological knowledge base or a literature search), as well as further assumptions about the properties of the network's transitions (e.g., the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an initial sketch which is extended by adding restrictions representing experimental data to a data-informed sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data.

AVAILABILITY

All software and data are freely available as a reproducible artefact at https://doi.org/10.5281/zenodo.7688740.

SUPPLEMENTARY INFORMATION

Supplementary data available online through Bioinformatics.

Rule-based modelling of biological systems using regulated rewriting

In systems biology, models play a crucial role in understanding studied systems. There are many modelling approaches, among which rewriting systems provide a framework for describing systems on a mechanistic level. Describing biochemical processes often requires incorporating knowledge on an abstract level to simplify the system description or substitute the missing details. For this purpose, we present regulation mechanisms, an extension of this formalism with additional controls on the rewriting process. We introduce several regulation mechanisms and apply them to a rule-based language, a notation suitable for modelling biological phenomena. Finally, we demonstrate the usage of such regulations on several case studies from the biochemical domain.

Systems Biology in ELIXIR: modelling in the spotlight

In this white paper, we describe the founding of a new ELIXIR Community - the Systems Biology Community - and its proposed future contributions to both ELIXIR and the broader community of systems biologists in Europe and worldwide. The Community believes that the infrastructure aspects of systems biology - databases, (modelling) tools and standards development, as well as training and access to cloud infrastructure - are not only appropriate components of the ELIXIR infrastructure, but will prove key components of ELIXIR's future support of advanced biological applications and personalised medicine. By way of a series of meetings, the Community identified seven key areas for its future activities, reflecting both future needs and previous and current activities within ELIXIR Platforms and Communities. These are: overcoming barriers to the wider uptake of systems biology; linking new and existing data to systems biology models; interoperability of systems biology resources; further development and embedding of systems medicine; provisioning of modelling as a service; building and coordinating capacity building and training resources; and supporting industrial embedding of systems biology. A set of objectives for the Community has been identified under four main headline areas: Standardisation and Interoperability, Technology, Capacity Building and Training, and Industrial Embedding. These are grouped into short-term (3-year), mid-term (6-year) and long-term (10-year) objectives.

Extracting individual characteristics from population data reveals a negative social effect during honeybee defence

Honeybees protect their colony against vertebrates by mass stinging and they coordinate their actions during this crucial event thanks to an alarm pheromone carried directly on the stinger, which is therefore released upon stinging. The pheromone then recruits nearby bees so that more and more bees participate in the defence. However, a quantitative understanding of how an individual bee adapts its stinging response during the course of an attack is still a challenge: Typically, only the group behaviour is effectively measurable in experiment; Further, linking the observed group behaviour with individual responses requires a probabilistic model enumerating a combinatorial number of possible group contexts during the defence; Finally, extracting the individual characteristics from group observations requires novel methods for parameter inference.

We first experimentally observed the behaviour of groups of bees confronted with a fake predator inside an arena and quantified their defensive reaction by counting the number of stingers embedded in the dummy at the end of a trial. We propose a biologically plausible model of this phenomenon, which transparently links the choice of each individual bee to sting or not, to its group context at the time of the decision. Then, we propose an efficient method for inferring the parameters of the model from the experimental data. Finally, we use this methodology to investigate the effect of group size on stinging initiation and alarm pheromone recruitment.

Our findings shed light on how the social context influences stinging behaviour, by quantifying how the alarm pheromone concentration level affects the decision of each bee to sting or not in a given group size. We show that recruitment is curbed as group size grows, thus suggesting that the presence of nestmates is integrated as a negative cue by individual bees. Moreover, the unique integration of exact and statistical methods provides a quantitative characterisation of uncertainty associated to each of the inferred parameters.

In this paper, our interdisciplinary team has significantly improved the understanding of how honeybees coordinate their actions during defence. Our first step was to measure the output behaviour of groups of bees under controlled experimental conditions. We then developed a model and methodology that allow us to quantify how the responsiveness to the alarm pheromone evolves during a defensive event, for a given group size. We show that recruitment becomes less effective as group size increases, thus revealing the existence of a negative social effect that acts on top of alarm pheromone communication. Our contribution is thus two-fold: on the computational side, we provide new tools to extract individual characteristics from population data, which is a challenging issue in the study of collective behaviour. On the biological side, we provide evidence that bees weight in their social context when making the decision to sting. We hypothesize that this may be an important mechanism to prevent recruitment from spinning out of control, ultimately preserving the colony from workforce depletion.

AEON.py: Python Library for Attractor Analysis in Asynchronous Boolean Networks

Summary

AEON.py is a Python library for the analysis of the long-term behaviour in very large asynchronous Boolean networks. It provides significant computational improvements over the state of the art methods for attractor detection. Furthermore, it admits the analysis of partially specified Boolean networks with uncertain update functions. It also includes techniques for identifying viable source-target control strategies and the assessment of their robustness with respect to parameter perturbations.

Availability and Implementation

All relevant results are available in supplementary materials. The tool is accessible through https://github.com/sybila/biodivine-aeon-py.

Supplementary information

Supplementary data are available online through Bioinformatics.

Exploring attractor bifurcations in Boolean networks

Background

Boolean networks (BNs) provide an effective modelling formalism for various complex biochemical phenomena. Their long term behaviour is represented by attractors–subsets of the state space towards which the BN eventually converges. These are then typically linked to different biological phenotypes. Depending on various logical parameters, the structure and quality of attractors can undergo a significant change, known as a bifurcation. We present a methodology for analysing bifurcations in asynchronous parametrised Boolean networks.

Results

In this paper, we propose a computational framework employing advanced symbolic graph algorithms that enable the analysis of large networks with hundreds of Boolean variables. To visualise the results of this analysis, we developed a novel interactive presentation technique based on decision trees, allowing us to quickly uncover parameters crucial to the changes in the attractor landscape. As a whole, the methodology is implemented in our tool AEON. We evaluate the method’s applicability on a complex human cell signalling network describing the activity of type-1 interferons and related molecules interacting with SARS-COV-2 virion. In particular, the analysis focuses on explaining the potential suppressive role of the recently proposed drug molecule GRL0617 on replication of the virus.

Conclusions

The proposed method creates a working analogy to the concept of bifurcation analysis widely used in kinetic modelling to reveal the impact of parameters on the system’s stability. The important feature of our tool is its unique capability to work fast with large-scale networks with a relatively large extent of unknown information. The results obtained in the case study are in agreement with the recent biological findings.

The need for standardisation in life science research - an approach to excellence and trust

Today, academic researchers benefit from the changes driven by digital technologies and the enormous growth of knowledge and data, on globalisation, enlargement of the scientific community, and the linkage between different scientific communities and the society. To fully benefit from this development, however, information needs to be shared openly and transparently. Digitalisation plays a major role here because it permeates all areas of business, science and society and is one of the key drivers for innovation and international cooperation. To address the resulting opportunities, the EU promotes the development and use of collaborative ways to produce and share knowledge and data as early as possible in the research process, but also to appropriately secure results with the European strategy for Open Science (OS). It is now widely recognised that making research results more accessible to all societal actors contributes to more effective and efficient science; it also serves as a boost for innovation in the public and private sectors. However  for research data to be findable, accessible, interoperable and reusable the use of standards is essential. At the metadata level, considerable efforts in standardisation have already been made (e.g. Data Management Plan and FAIR Principle etc.), whereas in context with the raw data these fundamental efforts are still fragmented and in some cases completely missing. The CHARME consortium, funded by the European Cooperation in Science and Technology (COST) Agency, has identified needs and gaps in the field of standardisation in the life sciences and also discussed potential hurdles for implementation of standards in current practice. Here, the authors suggest four measures in response to current challenges to ensure a high quality of life science research data and their re-usability for research and innovation.

Executable biochemical space for specification and analysis of biochemical systems

Computational systems biology provides multiple formalisms for modelling of biochemical processes among which the rule-based approach is one of the most suitable. Its main advantage is a compact and precise mechanistic description of complex processes. However, state-of-the-art rule-based languages still suffer several shortcomings that limit their use in practice. In particular, the elementary (low-level) syntax and semantics of rule-based languages complicate model construction and maintenance for users outside computer science. On the other hand, mathematical models based on differential equations (ODEs) still make the most typical used modelling framework. In consequence, robust re-interpretation and integration of models are difficult, thus making the systems biology paradigm technically challenging. Though several high-level languages have been developed at the top of rule-based principles, none of them provides a satisfactory and complete solution for semi-automated description and annotation of heterogeneous biophysical processes integrated at the cellular level. We present the second generation of a rule-based language called Biochemical Space Language (BCSL) that combines the advantages of different approaches and thus makes an effort to overcome several problems of existing solutions. BCSL relies on the formal basis of the rule-based methodology while preserving user-friendly syntax of plain chemical equations. BCSL combines the following aspects: the level of abstraction that hides structural and quantitative details but yet gives a precise mechanistic view of systems dynamics; executable semantics allowing formal analysis and consistency checking at the level of the language; universality allowing the integration of different biochemical mechanisms; scalability and compactness of the specification; hierarchical specification and composability of chemical entities; and support for genome-scale annotation.

Robustness analysis of stochastic biochemical systems

We propose a new framework for rigorous robustness analysis of stochastic biochemical systems that is based on probabilistic model checking techniques. 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. We have applied the framework 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 have successfully extended previous studies performed on deterministic models (ODE) and showed 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.