MOTIVATION: System control can be used to provide new insights into the dynamics of biological systems. A key application is the identification of therapeutic targets in silico, which requires an executable model of the system's dynamics. However, such models are typically underspecified due to incomplete mechanistic knowledge. RESULTS: We introduce a novel computational framework that employs control-guided model refinement, predicting informative perturbation experiments to reduce knowledge gaps. The approach is based on partially specified Boolean networks (PSBNs), which enable direct integration of uncertain or incomplete information into executable models. We further extend the framework to handle oscillatory phenotypes as explicit control targets. The applicability of the method is demonstrated on receptor-tyrosine kinase (RTK) signaling, with a focus on fibroblast growth factor signaling in the context of skeletal dysplasias and cancer. We obtain several new insights into modelling of the FGFR3-MAPK pathway. AVAILABILITY AND IMPLEMENTATION: Code and datasets are available at https://doi.org/10.5281/zenodo.16886813.

BACKGROUND: Stochastic models are commonly employed in the system and synthetic biology to study the effects of stochastic fluctuations emanating from reactions involving species with low copy-numbers. Many important models feature complex dynamics, involving a state-space explosion, stiffness, and multimodality, that complicate the quantitative analysis needed to understand their stochastic behavior. Direct numerical analysis of such models is typically not feasible and generating many simulation runs that adequately approximate the model's dynamics may take a prohibitively long time. RESULTS: We propose a new memoization technique that leverages a population-based abstraction and combines previously generated parts of simulations, called segments, to generate new simulations more efficiently while preserving the original system's dynamics and its diversity. Our algorithm adapts online to identify the most important abstract states and thus utilizes the available memory efficiently. CONCLUSION: We demonstrate that in combination with a novel fully automatic and adaptive hybrid simulation scheme, we can speed up the generation of trajectories significantly and correctly predict the transient behavior of complex stochastic systems.

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 AND IMPLEMENTATION: All software and data are freely available as a reproducible artefact at https://doi.org/10.5281/zenodo.7688740.

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 at Bioinformatics online.

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.

Edge-coloured directed graphs provide an essential structure for modelling and analysis of complex systems arising in many scientific disciplines (e.g. feature-oriented systems, gene regulatory networks, etc.). One of the fundamental problems for edge-coloured graphs is the detection of strongly connected components, or SCCs. The size of edge-coloured graphs appearing in practice can be enormous both in the number of vertices and colours. The large number of vertices prevents us from analysing such graphs using explicit SCC detection algorithms, such as Tarjan's, which motivates the use of a symbolic approach. However, the large number of colours also renders existing symbolic SCC detection algorithms impractical. This paper proposes a novel algorithm that symbolically computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs $O(p \cdot n \cdot log~n)$ symbolic steps, where $p$ is the number of colours and $n$ is the number of vertices. We evaluate the algorithm using an experimental implementation based on binary decision diagrams (BDDs). Specifically, we use our implementation to explore the SCCs of a large collection of coloured graphs (up to $2^{48}$) obtained from Boolean networks -- a modelling framework commonly appearing in systems biology.

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.

Abstract Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one. Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, calledinterleaved transition guided reduction(ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states. We evaluate the suggested heuristic on an extensive collection of 125 real-world biologically motivated systems. We show that ITGR can easily handle all these models while being either the only method to finish, or providing at least an order-of-magnitude speedup over existing state-of-the-art methods. We then use a set of synthetic benchmarks to demonstrate that the technique also consistently scales to graphs with more than $$2^{1000}$$ 21000 vertices, which was not possible using previous methods.

Abstract Problems arising in many scientific disciplines are often modelled using edge-coloured directed graphs. These can be enormous in the number of both vertices and colours. Given such a graph, the original problem frequently translates to the detection of the graph’s strongly connected components, which is challenging at this scale. We propose a new, symbolic algorithm that computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs $$O(p\cdot n\cdot \log n)$$ O ( p · n · log n ) symbolic steps, where p is the number of colours and n the number of vertices. We evaluate the algorithm using an experimental implementation based on Binary Decision Diagrams (BDDs) and large (up to $$2^{48}$$ 2 48 ) coloured graphs produced by models appearing in systems biology.

Boolean networks (BNs) provide an effective modelling tool for various phenomena from science and engineering. Any long-term behaviour of a BN eventually converges to a so-called attractor. Depending on various logical parameters, the structure and quality of attractors can undergo a significant change, known as a bifurcation. We present a tool for analysing bifurcations in asynchronous parametrised Boolean networks. To fight the state-space and parameter-space explosion problem the tool uses a parallel semi-symbolic algorithm.

Formal analysis of non-linear continuous and hybrid systems is a hot topic. A common approach builds on computing a suitable finite discrete abstraction of the continuous system. In this paper, we propose a facetal abstraction which eliminates certain drawbacks of existing abstractions. The states of our abstraction are built primarily from facets of a polytopal partitioning of the system's state space taking thus into account the flow of the continuous dynamics and leading to global over-approximation. The transition system construction is based on queries solved by a δ-decision SMT-solver. The method is evaluated on several case studies.

Digital bifurcation analysis is a new algorithmic method for exploring how the behaviour of a parameter-dependent computer system varies with a change in its parameters and, in particular, for identification of bifurcation points where such variation becomes dramatic. We have developed the method in an analogy with the traditional bifurcation theory and have it successfully applied to models taken from systems biology. In this case study paper, we demonstrate the appropriateness and usefulness of the digital bifurcation analysis as a push-button alternative to the classical approaches as traditionally used for analysing the stability of TCP/IP protocols. We consider two typical examples (congestion control and buffer sizes throughput influence) and show that the method provides the same results as obtained with classical non-automatic analytical and numerical methods.

An important problem in current computational systems biology is to analyze models of biological systems dynamics under parameter uncertainty. This paper presents a novel algorithm for parameter synthesis based on parallel model checking. The algorithm is conceptually universal with respect to the modeling approach employed. We introduce the algorithm, show its scalability, and examine its applicability on several biological models.

The current interest in systems biology is to gain a better understanding of how the complex dynamic behaviour of the cell emerges from mutual interactions of molecular species. When solving such a nontrivial goal, biological data have to be necessarily integrated with mathematical modelling and computer analysis. Since the key aspect of biological modelling is based on unifying several kinds of data captured in terms of large-scale biological networks, scalable and automatized methods are necessary to obtain novel predictions and understanding. In this review, we provide a brief description of the tool DiVinE adapted for automatized analysis of biological systems dynamics. The tool employs high-performance computing techniques to enable analysis of large models.

The work on a visual formalism for specification of concurrent systems is presented. It is proposed to match requirements of state-of-the-art component-based design methods. Special emphasis is given to specification of heterogeneous systems in which the different models of computation can be mixed together. We briefly summarize recent research related to the topic and give a sketch of the basic ideas for definition of the proposed language. The already achieved results of our work are presented as well.