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 ADF. Our approach is inspired by the recently discovered equivalence between Boolean Networks (BNs) and ADFs, 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.

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 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.

International audience

International audience

MOTIVATION: Boolean networks are popular dynamical models of cellular processes in systems biology. Their attractors model phenotypes that arise from the interplay of key regulatory subcircuits. A succession diagram (SD) describes this interplay in a discrete analog of Waddington's epigenetic attractor landscape that allows for fast identification of attractors and attractor control strategies. Efficient computational tools for studying SDs are essential for the understanding of Boolean attractor landscapes and connecting them to their biological functions. RESULTS: We present a new approach to SD construction for asynchronously updated Boolean networks, implemented in the biologist's Boolean attractor landscape mapper, biobalm. We compare biobalm to similar tools and find a substantial performance increase in SD construction, attractor identification, and attractor control. We perform the most comprehensive comparative analysis to date of the SD structure in experimentally-validated Boolean models of cell processes and random ensembles. We find that random models (including critical Kauffman networks) have relatively small SDs, indicating simple decision structures. In contrast, nonrandom models from the literature are enriched in extremely large SDs, indicating an abundance of decision points and suggesting the presence of complex Waddington landscapes in nature. AVAILABILITY AND IMPLEMENTATION: The tool biobalm is available online at https://github.com/jcrozum/biobalm. Further data, scripts for testing, analysis, and figure generation are available online at https://github.com/jcrozum/biobalm-analysis and in the reproducibility artefact at https://doi.org/10.5281/zenodo.13854760.

Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).

Boolean Networks (BNs) are an efficient modeling formalism with applications in various research fields such as mathematics, computer science, and more recently systems biology. One crucial problem in the BN research is to enumerate all fixed points, which has been proven crucial in the analysis and control of biological systems. Indeed, in that field, BNs originated from the pioneering work of R. Thomas on gene regulation and from the start were characterized by their asymptotic behavior: complex attractors and fixed points. The former being notably more difficult to compute exactly, and specific to certain biological systems, the computation of stable states (fixed points) has been the standard way to analyze those BNs for years. However, with the increase in model size and complexity of Boolean update functions, the existing methods for this problem show their limitations. To our knowledge, the most efficient state-of-the-art methods for the fixed point enumeration problem rely on Answer Set Programming (ASP). Motivated by these facts, in this work we propose two new efficient ASP-based methods to solve this problem. We evaluate them on both real-world and pseudo-random models, showing that they vastly outperform four state-of-the-art methods as well as can handle very large and complex models.

MOTIVATION: Boolean networks are simple but efficient mathematical formalism for modelling complex biological systems. However, having only two levels of activation is sometimes not enough to fully capture the dynamics of real-world biological systems. Hence, the need for multi-valued networks (MVNs), a generalization of Boolean networks. Despite the importance of MVNs for modelling biological systems, only limited progress has been made on developing theories, analysis methods, and tools that can support them. In particular, the recent use of trap spaces in Boolean networks made a great impact on the field of systems biology, but there has been no similar concept defined and studied for MVNs to date. RESULTS: In this work, we generalize the concept of trap spaces in Boolean networks to that in MVNs. We then develop the theory and the analysis methods for trap spaces in MVNs. In particular, we implement all proposed methods in a Python package called trapmvn. Not only showing the applicability of our approach via a realistic case study, we also evaluate the time efficiency of the method on a large collection of real-world models. The experimental results confirm the time efficiency, which we believe enables more accurate analysis on larger and more complex multi-valued models. AVAILABILITY AND IMPLEMENTATION: Source code and data are freely available at https://github.com/giang-trinh/trap-mvn.

Boolean networks (BNs)play a crucial role in modeling and analyzing biological systems. One of the central issues in the analysis of BNs is attractor detection, i.e., identification of all possible attractors. This problem becomes more challenging for large asynchronous random Boolean networks (ARBNs)because of the asynchronous and non-deterministic updating scheme. In this paper, we present and formally prove several relations between feedback vertex sets (FVSs)and dynamics of BNs. From these relations, we propose an FVS-based method for detecting attractors in ARBNs. Our approach relies on the principle of removing arcs in the state transition graph to get a candidate set and the reachability property to filter the candidate set. We formally prove the correctness of our method and show its efficiency by conducting experiments on real biological networks and randomly generated N- K networks. The obtained results are very promising since our method can handle large networks whose sizes are up to 101 without using any network reduction technique.

Deterministic asynchronous Boolean networks play a crucial role in modeling and analysis of gene regulatory networks. In this paper, we focus on a typical type of deterministic asynchronous Boolean networks called deterministic generalized asynchronous random Boolean networks (DGARBNs). We first formulate the extended state transition graph, which captures the whole dynamics of a DGARBN and paves potential ways to analyze this DGARBN. We then propose two SMT-based methods for attractor detection and optimal control of DGARBNs. These methods are implemented in a JAVA tool called DABoolNet. Two experiments are designed to highlight the scalability of the proposed methods. We also formally state and prove several relations between DGARBNs and other models including deterministic asynchronous models, block-sequential Boolean networks, generalized asynchronous random Boolean networks, and mixed-context random Boolean networks. Several case studies are presented to show the applications of our methods.

Attractor detection in Asynchronous Boolean Networks (ABNs) is very challenging due to the high complexity of the state transition graph of an ABN. Recently, an efficient method (called FVS-ARBN) has been proposed for exactly finding attractors of an ABN. FVS-ARBN uses a Feedback Vertex Set (FVS) to get a candidate set of states, then filters out this set by checking the reachability in ABNs. This method gives promising results; however, it still needs to be improved to handle larger networks. In this paper, we propose a new method (named iFVS-ABN) that includes two improvements to FVS-ARBN. First, we propose a reasonable combination of multiple existing techniques to efficiently check the reachability in ABNs. Second, we formally state and prove a relation between a Negative Feedback Vertex Set (NFVS) and the dynamics of an ABN. Based on this relation, we propose to use an NFVS instead of an FVS to get the candidate set of states. Experimental results show that the two improvements are effective and the improved method outperforms the original one.

Boolean networks (BNs) play a crucial role in modeling and analyzing biological systems especially gene regulatory networks. One of the central issues in the analysis of BNs is attractor detection, i.e., detecting all possible attractors of a BN. This problem becomes more challenging for large asynchronous random Boolean networks (ARBNs) because of the asynchronous and non-deterministic updating scheme. In this paper, we state and prove several relations between dynamics of ARBNs and generalized asynchronous random Boolean networks (GARBNs). Based on these relations, we propose an efficient method called ApproARBN for approximating attractors of ARBNs. The experimental results on real biological networks justify the accuracy of ApproARBN and show the efficiency of ApproARBN since ApproARBN outperforms two state-of-the-art methods and can handle large networks whose sizes are up to 101 nodes.

Recently, Wireless Sensor Networks (WSNs) attract many researches due to their real applications. WSN is actually a network whose main components are sensors and channels. Based on applications, these components can be worked independently or separately with each others to capture information, process and send it to sink. However, in congestion-based aspect, most researches are assumed that environmental working of components are perfect, i.e. they omit packet-loss aspect due to failed sensors or broken links. This causes a limitation to rationally represent a WSN. Thus, in this proposal, using the reliable probability property, we define a Discrete Time Stochastic Petri Net Model for congestion detection on WSN in order to represent all working scenarios for components on the one hand, and calculate the congestion probability in the network on the other hand. After that, we also present a new algorithm to analyse on that model. Our straight example through this paper emphasises the idea of our model.