ABSTRACT. In this work, we study the source-target control problem of Boolean networks, which has important applications for cellular re- programming. More specifically, we want to perturb the input Boolean network such that it leaves a predetermined source attractor to eventu- ally find itself in the target attractor. We use edge perturbations, which modify the update functions of a Boolean network without necessarily setting them to constants. This work improves an existing method in which edge perturbations are used to eliminate all but the target attrac- tor. Both approaches are based on Thomas’ first rule: the existence of at least one positive cycle in the interaction graph of a dynamical system is a necessary condition for the existence of multiple steady states. Thus, if all positive cycles are removed, the resulting dynamical system has a single steady state. This requires removing a subset of edges so that at least one edge of every cycle in the graph is perturbed: the feedback edge set. Information on the source and target attractors allows to reduce the number of relevant feedback edge sets and, subsequently, candidate perturbations. We propose a carefully designed strategy that combines exhaustive search and a heuristic inspired by Simulated Annealing to ef- fectively reduce the number of required perturbations with respect to the feedback edge set. We evaluate our method on a wide array of Boolean networks from the literature to demonstrate its efficacy and efficiency.

ABSTRACT. Biochemical systems involve both the flow of matter, in which entities transform into one another via reactions, and the flow of information, in which entities regulate which reactions may occur. Boolean networks capture the latter; reaction networks capture the former. Yet no unified qualitative formalism treats regulated reactions as its principal objects of study, despite their prominence in standards such as the Systems Biology Graphical Notation Process Description (SBGN-PD) language. We introduce modulation-reaction networks (MR-networks), a mathematical framework in which entities modulate reactions through activations and inhibitions, and study their synchronous Boolean semantics. To reason about MR-networks we develop Modulation-Reaction Logic (MRL), a hybrid modal mu-calculus whose modalities reason about the structure of the network and whose fixed-point operators capture temporal evolution of the computation. We establish a collection of validities, including a complete characterisation of the one-step update rule, and demonstrate the expressive power of MRL by formalising properties of biological interest such as reachability, sustained production, and presence of attractors. We show that MRL admits model-checking via an evaluation game, and introduce a bisimulation relation for MR-networks, which is proved to be invariant for all MRL-formulas. As a step towards a biologically more realistic computational model, we sketch the asynchronous semantics of MR-networks, and outline how the developments for the synchronous case transfer to the study of the asynchronous one.

ABSTRACT. Qualitative models provide crucial instruments for modelling complex biological systems. While advances in automated reasoning and symbolic encodings have enabled rigorous inference of these models from data, the process remains highly fragile. First, biological measurement errors inevitably propagate into formal model specifications. Second, when a specification becomes unsatisfiable, distinguishing between fundamental design flaws and minor technical errors is notoriously difficult. This uncertainty often leads to under-specification, as it is unclear which observations are still ``safe'' to incorporate. To overcome these challenges, we introduce a robust inference method based on weighted MaxSMT. By encoding uncertain biological observations as weighted soft constraints, our approach enables the solver to identify a model best reflecting the observations, even with some conflicting constraints. Our method allows for Boolean and multi-valued variable domains, alongside observations derived from discretisation (level constraints) and differential expression (ordering constraints). We show our approach can be used to successfully infer neural cell differentiation models from prior-knowledge networks with 200--1300 genes using ordering constraints on all included genes.

ABSTRACT. Biological regulatory networks can be represented by computational models, which allow the study and analysis of biological behaviours, therefore providing a better understanding of a given biological process. However, as new information is acquired, biological models may need to be revised in order to also account for this new information. Current model revision tools are scarce and often lack the flexibility to integrate with broader analysis workflows. Here, we present pyModRev, an enhanced iteration of the model revision tool ModRev, capable of verifying the consistency of Boolean regulatory models, and finding minimal repairs in case of inconsistency. pyModRev supports model validation against both steady state observations as well as time-series data, being able to consider different update schemes simultaneously. pyModRev supports different model formats, and is available as a Python package in PyPI, for easy integration with other model analysis tools, significantly improving accessibility and utility for the logical modelling community.

ABSTRACT. Kappa is a graph-rewriting language originally developed for modeling molecular interactions in cellular processes. A key feature of Kappa models is that, inspired by organic chemistry, interaction rules operate on patterns i.e., partially specified molecular species, thus allowing compact descriptions of otherwise large or even infinite models. In this paper, we propose and implement a framework for statistical model checking for stochastic Kappa models against properties written in bounded linear temporal logic (BLTL). A key feature of our approach is that temporal properties operate over Kappa patterns, making the specification language native to Kappa and avoiding the expensive—and sometimes theoretically impossible translation of the model into an equivalent chemical reaction network with a finite number of species. Concretely, given a Kappa model and a property, we first instrument the model by introducing additional variables and observables that track the truth value of each atomic proposition. For each simulated trace, the BLTL formula satisfaction is evaluated using an offline monitoring procedure. Finally, the satisfaction probability is statistically estimated from repeated model simulations. The proposed model checking framework enables a systematic exploration of behavioral properties of Kappa models, that is computationally efficient while able to capture stochastic and finite size effects with any predefined desired accuracy/precision. As such, it can serve in applications for e.g. model selection, property-driven parameter exploration, or robustness analysis. The framework is illustrated on representative case studies from systems biology and swarm robotics.

ABSTRACT. Bursty transcription in single cells typically produces over-dispersed, skewed, and sometimes heavy-tailed expression distributions that are explained by two-state Markov models of the promoters. While the gold standard for simulation is exact stochastic sampling with Gillespie's algorithm, obtaining thousands of timed traces is computationally costly. Surrogate models based on stochastic differential equations (SDEs) are widely used to speed up this simulation process. An example is the Chemical Langevin Equation based on Gaussian noise, which, however, does not capture heavy-tailed noise. In this work, we present a unified SDE framework that combines deterministic drift, Gaussian fluctuations, and additive sporadic jumps of arbitrary distributions, and provide an open-source Python implementation, bcrnnoise. The framework subsumes standard surrogate models and allows for vectorized generation of batches of transcription traces. We assess computational speed and accuracy of common surrogate models along with new models, showing that high accuracy can be obtained while reducing computational cost up to two orders of magnitude.

ABSTRACT. Reaction Systems (RSs) provide a successful qualitative modelling framework inspired by biochemical reactions. In a RS a computation starts from a initial state given by a set of entities and each following computation state is determined by the application of all the enabled reactions to the previous state. RSs can also model the interaction with the environment. Each entity can either be present or absent in a computation state, as a crisp boolean condition, and also reactions are (or not) enabled under crisp conditions. This framework has proved to have many applications for modelling biomedical and computer science systems, but it can become restrictive when laboratory measurements exhibit graded concentrations, partial inhibition, and noise. We thus introduce Mamdani-driven Fuzzy Reaction Systems (M-FRS), as a graded conservative extension of RSs. Each reaction in the style of RSs is now interpreted as a Mamdani rule, and we formalise a single four-stage fuzzy inference cycle (fuzzification, rule evaluation, aggregation, optional defuzzification) which defines a deterministic discrete-time graded update operator. Fuzzy inference yields a discrete dynamical system. As a first case study, we develop a compact M-FRS model of the hypothalamic--pituitary--thyroid axis.

ABSTRACT. Kappa offers a modeling environment to describe, simulate, and reason about rule-based models. It has been used to model protein-protein interaction networks, especially models of signaling pathways. Kappa comes with a static analyzer, KaSa, to assist the modeler and assess the consistency of the models. Although efficient, KaSa is sometimes too slow to reason while modifying large models or when editing models within the user interface. Here, we propose an incremental version that updates the result of the current analysis at each model modification. Our approach relies on the use of an abstraction of the relationships between the rules of the model and the properties that they induce. Partial evaluation is used when some rules are removed, to exclude the results that derive from the removed rules. Adding rules is done classically by resuming the iterations of the analysis algorithm. This incremental analysis is available on the command-line or as an electron app, and it is evaluated on examples from the literature.