arXiv subjects

Samuel Pastva

Publications and source records attributed to Samuel Pastva.

11 recordsLinked to original sources

arXiv2026

Inference of Qualitative Models from Steady-State Data via Weighted MaxSMT

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.

q-bio.MN↗

arXiv2026

BAss: Symbolic Reasoning in Abstract Dialectical Frameworks

We present BAss (BDD-based ADF symbolic solver), a novel analysis tool for Abstract Dialectical Frameworks (ADFs) based on Binary Decision Diagrams (BDDs). It supports the fully symbolic computation of all admissible, complete, and preferred interpretations, as well as two-valued and stable models of an ADFs. Our approach is inspired by the recently discovered equivalence between Boolean Networks (BNs) and ADFs by Heyninck et al. (2024) and Azpeitia et al. (2024), significantly extending current BDD-based tools bioLQM, AEON, and adf-bdd. We conducted experiments on a large-scale collection of real-world models from both the BN and ADF communities. Our results show that BAss dramatically outperforms previous BDD-based tools and is competitive (even significantly better in some cases) with state-of-the-art SAT/ASP-based methods, particularly in scenarios involving large solution spaces. Notably, BAss is able to enumerate all fixed points or minimal trap spaces of certain biological networks beyond the reach of existing tools, thereby enabling new analysis and case studies in systems biology. These results highlight the practical relevance of symbolic reasoning for complex real-world applications, particularly in systems biology and formal argumentation.

cs.LO↗

arXiv2026

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology

The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand. We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

cs.LO↗

arXiv2026

Relating biomarkers and phenotypes using dynamical trap spaces

Connecting the dynamics of biomolecular networks to experimentally measurable cell phenotypes remains a central challenge in systems biology. Here we introduce a model-based definition of phenotype as a partial steady state that is committed to a certain dynamical outcome while otherwise being minimally constrained. We focus on Boolean models and define \emph{dynamical phenotypes} as complete trap spaces that maximally specify a chosen set of phenotype-determining nodes that correspond to biomarkers while keeping external inputs unconstrained. We show that dynamical phenotypes can be efficiently identified without full attractor enumeration. Using four published models, including a 70-node Boolean model of T cell differentiation, we show that dynamical phenotypes recover known cell types and activation states, and indicate the environmental conditions ensuring their existence. We also propose a method to identify informative phenotype-determining nodes based on the canalization of the Boolean functions. This method reveals biologically relevant cell state information that is complementary to the phenotypes manually defined by model creators and is validated by two attractor-based approaches. Our results demonstrate that dynamical phenotypes provide a scalable framework for linking model structure, external inputs, and phenotypic outcomes, and offer a principled tool for model-guided biomarker selection.

q-bio.MN↗

arXiv2025

Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks

Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and artificial intelligence. A crucial property of BNs is the presence of trap spaces -- subspaces of the state space that, once entered, cannot be exited. Minimal trap spaces, in particular, play a significant role in analyzing the long-term behavior of BNs, making their efficient enumeration and counting essential. The fixed points in BNs are a special case of minimal trap spaces. In this work, we formulate several meaningful counting problems related to minimal trap spaces and fixed points in BNs. These problems provide valuable insights both within BN theory (e.g., in probabilistic reasoning and dynamical analysis) and in broader application areas, including systems biology, abstract argumentation, and logic programming. To address these computational challenges, we propose novel methods based on {\em approximate answer set counting}, leveraging techniques from answer set programming. Our approach efficiently approximates the number of minimal trap spaces and the number of fixed points without requiring exhaustive enumeration, making it particularly well-suited for large-scale BNs. Our experimental evaluation on an extensive and diverse set of benchmark instances shows that our methods significantly improve the feasibility of counting minimal trap spaces and fixed points, paving the way for new applications in BN analysis and beyond.

cs.LO↗

arXiv2025

On the number of asynchronous attractors in AND-NOT Boolean networks

Boolean Networks (BNs) describe the time evolution of binary states using logic functions on the nodes of a network. They are fundamental models for complex discrete dynamical systems, with applications in various areas of science and engineering, and especially in systems biology. A key aspect of the dynamical behavior of BNs is the number of attractors, which determines the diversity of long-term system trajectories. Due to the noisy nature and incomplete characterization of biological systems, a stochastic asynchronous update scheme is often more appropriate than the deterministic synchronous one. AND-NOT BNs, whose logic functions are the conjunction of literals, are an important subclass of BNs because of their structural simplicity and their usefulness in analyzing biological systems for which the only information available is a collection of interactions among components. In this paper, we establish new theoretical results regarding asynchronous attractors in AND-NOT BNs. We derive two new upper bounds for the number of asynchronous attractors in an AND-NOT BN based on structural properties (strong even cycles and dominating sets, respectively) of the AND-NOT BN. These findings contribute to a more comprehensive understanding of asynchronous dynamics in AND-NOT BNs, with implications for attractor enumeration and counting, as well as for network design and control.

cs.DM↗

arXiv2024

An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks?

Asynchronous Boolean networks are a type of discrete dynamical system in which each variable can take one of two states, and a single variable state is updated in each time step according to pre-selected rules. Boolean networks are popular in systems biology due to their ability to model long-term biological phenotypes within a qualitative, predictive framework. Boolean networks model phenotypes as attractors, which are closely linked to minimal trap spaces (inescapable hypercubes in the system's state space). In biological applications, attractors and minimal trap spaces are typically in one-to-one correspondence. However, this correspondence is not guaranteed: motif-avoidant attractors (MAAs) that lie outside minimal trap spaces are possible. MAAs are rare and (despite recent efforts) poorly understood. Here we summarize the current state of knowledge regarding MAAs and present several novel observations regarding their response to node deletion reductions and linear extensions of edges. We conduct large-scale computational studies on an ensemble of 14,000 models derived from published Boolean models of biological systems, and more than 100 million Random Boolean Networks. Our findings quantify the rarity of MAAs (in particular, we found no MAAs in the biological models), but highlight the role of network reduction in introducing MAAs into the dynamics. We also show that MAAs are fragile to linear extensions: in sparse networks, even a single linear node can disrupt virtually all MAAs. Motivated by this observation, we improve the upper bound on the number of delays needed to disrupt a motif-avoidant attractor.

q-bio.MN↗

arXiv2022

Robust Control of Partially Specified Boolean Networks

Regulatory networks (RNs) are a well-accepted modelling formalism in computational systems biology. The control of RNs is currently receiving a lot of attention because it provides a computational basis for cell reprogramming -- an attractive technology developed in regenerative medicine. By solving the control problem, we learn which parts of a biological system should be perturbed to stabilise the system in the desired phenotype. We allow the specification of the Boolean model representing a given RN to be incomplete. To that end, we utilise the formalism of partially specified Boolean networks which covers every possible behaviour of unspecified parts of the system. Such an approach causes a significant state explosion. This problem is addressed by using symbolic methods to represent both the unspecified model parts and all possible perturbations of the system. Additionally, to make the control design efficient and practically applicable, the optimal control should be minimal in terms of size. Moreover, in a partially specified model, a control may achieve the desired stabilisation only for a subset of the possible fully specified model instantiations. To address these aspects, we utilise several quantitative measures. Apart from the size of perturbation, we also examine its robustness -- a portion of instantiations for which the control is applicable. We show that proposed symbolic methods solving the control problem for partially specified BNs are efficient and scale well. We also evaluate the robustness metrics in cases of all three studied control types. The robustness metric tells us how big a proportion of fully defined systems the given perturbation works. Our experiments support the hypothesis that one-step perturbations may be less robust than temporary or permanent perturbations. This is a full version of a paper that is submitted to a journal.

eess.SY↗

arXiv2021

Regulated Multiset Rewriting Systems

Multiset rewriting systems provide a formalism particularly suitable for the description of biological systems. We present an extension of this formalism with additional controls on the derivations as a tool for reducing possible non-deterministic behaviour by providing additional knowledge about the system. We introduce several regulation mechanisms and compare their generative power.

cs.FL↗

arXiv2021

BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs

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.

cs.DS↗

arXiv2020

Parallel One-Step Control of Parametrised Boolean Networks

Boolean network (BN) is a simple model widely used to study complex dynamic behaviour of biological systems. Nonetheless, it might be difficult to gather enough data to precisely capture the behavior of a biological system into a set of Boolean functions. These issues can be dealt with to some extent using parametrised Boolean networks (ParBNs), as it allows to leave some update functions unspecified. In this paper, we attack the control problem for ParBNs with asynchronous semantics. While there is an extensive work on controlling BNs without parameters, the problem of control for ParBNs has not been in fact addressed yet. The goal of control is to ensure the stabilisation of a system in a given state using as few interventions as possible. There are many ways to control BN dynamics. Here, we consider the one-step approach in which the system is instantaneously perturbed out of its actual state. A naive approach to handle control of ParBNs is using parameter scan and solve the control problem for each parameter valuation separately using known techniques for non-parametrised BNs. This approach is however highly inefficient as the parameter space of ParBNs grows doubly-exponentially in the worst case. In this paper, we propose a novel semi-symbolic algorithm for the one-step control problem of ParBNs, that builds on a symbolic data structures to avoid scanning individual parameters. We evaluate the performance of our approach on real biological models.

q-bio.MN↗