SuppSupplement references

#  mpbn: a simple tool for efficient edition and analysis of elementary
properties of Boolean networks

Van-Giang Trinh1, Belaid Benhamou1, and Loïc Paulevé2

(  1LIRICA team, LIS, Aix-Marseille University, Marseille 13397, France
2Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR5800, F-33400 Talence, France
)

Abstract. The tool mpbn offers a Python programming interface for an easy
interactive editing of Boolean networks and the efficient computation of
elementary properties of their dynamics, including fixed points, trap spaces,
and reachability properties under the Most Permissive update mode. Relying on
Answer-Set Programming logical framework, we show that mpbn is scalable to
models with several thousands of nodes and is one of the best-performing tool
for computing minimal and maximal trap spaces of Boolean networks, a key
feature for understanding and controling their stable behaviors. The tool is
available at https://github.com/bnediction/mpbn.

##  1 Introduction

Boolean Networks (BNs) are fundamental models of gene regulation and
signalling networks dynamics [1, 2, 3], with decades of extensive theoretical
and practical research. The community developed numerous software tools which
implement various algorithms for their analysis [4, 5, 6, 7, 8, 9, 10], and
their edition [4, 5, 6]. Over the years, BNs have become a versatile formal
modeling framework, and many analysis algorithms have been built on elementary
properties of BNs, such as fixed points, trap spaces, and dynamical properties
[9]. However, with the constant increase in model size and complexity of
Boolean update functions, these previous tools show their performance
limitations. Moreover, most of them do not support interactive and easy-to-use
edition and revision of Boolean network definitions, which, coupled with basic
dynamical analyses, would enable seamless experimentation, including for
teaching.

Motivated by the above factors, mpbn offers a simple interface for
manipulating BNs and for performing efficient analysis of elementary
properties, namely fixed points, trap spaces, as well as transition graph
computation with various update modes, and including most permissive
reachability [9].

##  2 Features

Formally, a BN is a function from binary vectors of dimension $n$ to
themselves, i.e., of the form $f:\\{0,1\\}^{n}\to\\{0,1\\}^{n}$. These binary
vectors are the states (or configurations) of the BN. In practice, BNs are
specified by $n$ Boolean functions $f_{i}:\\{0,1\\}^{n}\to\\{0,1\\}$ for each
component $i\in\\{1,\dots,n\\}$. Most of the time, $f_{i}$ is expressed as a
propositional logic formula, i.e., with Boolean variables $x_{1},\dots,x_{n}$
and logical connectors. For example, $f_{2}(x)=x_{1}\lor\neg(x_{3}\land
x_{4})$, where $\land$, $\lor$, $\neg$ are respectively the conjunction,
disjunction, and negation operators. Also, instead of numbers, components are
usually referred to as names (e.g., gene name). In that case, we often write a
specification like “$B:=A\lor\neg(C\land D)$” instead of the former $f_{2}$
expression.

mpbn is an open-source Python module which offers both a simple programming
interface, and command line utilities. We present here its main features.

###  2.1 Model edition

In mpbn, a BN is implemented as a map associating component names to their
Boolean functions, expressed in propositional logic. It directly supports
loading models from the BooleanNet format [4] (.bnet) that is prevalent in the
BN research community, and most other usual formats through the biolqm library
[11]. A model can be created _ab initio_ in mpbn and the map can be updated as
standard Python map (dict) objects using the BooleanNet format. For example:

⬇

f = mpbn.MPBooleanNetwork("file.bnet")

f["B"] = "A | !(C & D)"

The internal representation of functions can be controlled. By default, mpbn
will convert the expression to its Disjunctive Normal Form (DNF), i.e.,
disjunction of conjunctions with negation only in front of variables. If a
variable appears both with and without a negation, mpbn will represent the
function using a Binary Decision Diagram (BDD). mpbn also offers the
possibility to preserve the structure as given. The internal representation
can influence the efficiency of the analysis. Model edited with mpbn can then
be exported to text files in the BooleanNet format for analysis with other
tools.

###  2.2 Most permissive dynamics

From a state of the BN, an _update mode_ enables to compute the next possible
states according to $f$. Traditionally, these update modes reflect the
different interleavings and simultaneous applications of component updates: in
_synchronous_ , all the components are updated at the same time, i.e., there
is one single next state being $f(x)$; in _asynchronous_ , only one component
is updated, leading to several choices for next states, of the form
$x_{1}\cdots x_{i-1}f_{i}(x)x_{i+1}\cdots x_{n}$. These dynamics can be
summarized by a State Transition Graph (STG), being a directed graph with an
edge from state $x$ to $y$ if the update mode enables that transition. In mpbn
it can be computed using f.dynamics("asynchronous") for instance. Other
classical update modes are also supported, and custom ones can be defined
using mpbn programming interface.

However, it has been shown in [9] that (a)synchronous dynamics can preclude
trajectories between states which are actually feasible with quantitative
models. The recently-introduced _Most Permissive_ (MP) update mode overcomes
this limitation, by guaranteeing to capture the trajectories of any
quantitative model being a _refinement_ of the BN, i.e., obtained by
introducing threshold, quantities, and kinetics [9]. Besides the computation
of the full MP dynamics with f.dynamics("mp"), mpbn also implements efficient
reachability tests: f.reachability(x,y) returns True if there exists an MP
trajectory from state $x$ to state $y$. Whereas this checking can be rapidly
intractable with the (a)synchronous mode, it has been demonstrated that in the
MP mode, it can scale to BNs with hundreds of thousands of nodes [9]. It is
worth noting that attractors in the MP mode of a BN (computed by
f.attractors()) are identical to minimal trap spaces of this BN [9]. In
addition, we can easily compute reachable MP attractors:
f.attractors(reachable_from=x) returns all the MP attractors reachable from
state $x$.

BNs employing the MP mode (MPBNs) have attracted much attention from
researchers in the field of logical modeling of biological systems, such as in
[12] using MPBNs to unravel new regulatory mechanisms of hematopoietic stem
cell aging, and in [13] for priorization of candidate genes influencing
epilepsies.

###  2.3 Fixed points and trap spaces

A _fixed point_ of a BN is a state $x$ such that $f(x)=x$. Fixed points are
extensively studied in biological modeling as the stable states of the system;
their analysis has been a starting point and a standard way for the BN
analysis. A trap space is a particular subcube of $\\{0,1\\}^{n}$ [14, 15]. A
subcube is characterized by a set of components having a fixed value and can
be represented as vectors $c$ in $\\{0,1,\ast\\}^{n}$. Its vertices are the
binary vectors $x=\\{0,1\\}^{n}$ where the components fixed in $c$ have the
same value in $x$. A subcube $c\in\\{0,1,\ast\\}^{n}$ is a _trap space_ if,
for each of its vertices $x$, $f(x)$ is also one of its vertices. Intuitively,
a trap space represents a “well-structured” part of the state space from which
it is impossible to escape by applying the functions of the BN. Notably, trap
spaces of a BN are _independent_ of its update mode. An _attractor_ is a non-
empty set of states such that once entered it, the BN’s dynamics cannot escape
from it. In contrast to trap spaces, attractors are _dependent_ of the
employed update mode of the BN. Note however that attractor computation is the
major analysis on BNs because attractors are linked to biological phenotypes
[2, 3], and there is a rich history of methods developed for it [16].

A trap space is _minimal_ if it does not contain any other trap space. Fixed
points are particular cases of minimal trap spaces where all components are
fixed [14]. Minimal trap spaces have been studied as good approximations of
attractors of BNs with the asynchronous update mode [7, 9, 17]. A trap space
is _maximal_ if it is not included in any other trap space, except the full
cube $\\{0,1\\}^{n}$ [14]. Maximal trap spaces are also employed for the
computation of attractors and for the computation of control strategies to
drive the system towards specific attractors [16], which play a role in
systems medicine. Furthermore, both minimal and maximal trap spaces (also ones
restricted to specific subcubes) have been used in several phenotype-based
control approaches of biological models [18, 19].

mpbn implements the enumeration of fixed points, minimal and maximal trap
spaces in BNs, possibly restricted to specific subcubes. Furthermore, it is
possible to perform a partial enumeration of them. Under the hood, the
computation is performed using logic programming with Answer-Set Programming
and the solver clingo [20].

From extensive benchmarks on real-world and randomly generated models, we
observed that mpbn is the sole tool able to address the computation of minimal
and maximal trap spaces and fixed points on the full range of models, and with
substantially better performance than state-of-the-art tools, especially in
large and complex models. Table 4 shows a summary of benchmark results for
minimal trap spaces on four sets of models with different properties: First,
the BBM repository [21] that consists of 212 published _biologically relevant_
BNs, ranging up to 321 variables. Second, the set of 23 other non-trivial and
_biologically relevant_ BNs collected from various bibliographic sources in
the literature, ranging up to 4691 variables (see Table 3 of Supplement for
more details). Third, a dataset of Very Large Boolean Networks (VLBN) [9]
consisting of 28 _random_ BNs, ranging up to 100,000 variables. And fourth, a
dataset (namely AEON) of 100 _random_ BNs of up to 1016 variables, generated
by using the generator provided in [22]. In our experiments, we compared mpbn
with pyboolnet [7] and trapmvn [23], which are to our best knowledge the most
recent and efficient tools for trap space and fixed point enumeration in BNs.
In addition, we only measured the time to compute the first result, which we
believe to make the most fair comparison among the considered techniques
because when there are multiple solutions, a benchmark is often testing the
technical ability of the implementation to enumerate them quickly, instead of
the actual problem-solving. Note that we here omit the benchmark results for
maximal trap spaces and fixed points because they do not reveal any
conclusions that are not covered by the minimal trap space case. All details
of the experiments are given in Section “Experiments” of Supplement.

Table 1: Summary of tool performance when computing the first minimal trap
space. Columns 2-7 give the number of models completed within the respective
time limit. 212 BBM models
---
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 141 | 167 | 186 | 190 | 200 | 200
trapmvn | 206 | 208 | 211 | 211 | 211 | 211
mpbn | 207 | 211 | 212 | 212 | 212 | 212
23 selected models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 4 | 5 | 5 | 8 | 10 | 10
trapmvn | 14 | 15 | 16 | 22 | 23 | 23
mpbn | 15 | 20 | 23 | 23 | 23 | 23
28 VLBN models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 0 | 7 | 8 | 14 | 20
mpbn | 4 | 8 | 16 | 20 | 28 | 28
100 AEON models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 6 | 47 | 96 | 100 | 100
mpbn | 100 | 100 | 100 | 100 | 100 | 100

###  2.4 Example of usage

For illustration, Figure 1 shows an example of usage for these computations
using the Python API. The command line utility of mpbn offers similar
features.

Figure 1: Example of usage within a Jupyter notebook

We consider a BN with three nodes ($a$, $b$, and $c$) and three associated
Boolean functions: $f_{a}=\neg b$, $f_{b}=\neg a$, and $f_{c}=\neg(a\land\neg
b)\land\neg c$. mpbn can load this BN from an input file in the BooleanNet
format. The input file can be located in the local machine or online. For
convenience, mpbn also supports inline initialization, and we use it here (see
Row In [2]). The list of Boolean functions of this BN is printed out in DNF
when typing f (see Row Out [2]). The influence graph of a BN is a signed
directed graph where a vertex denotes a node of the BN and an edge
$(u,sign,v)$ denotes the effect (activating if $sign=+$ and inhibiting if
$sign=-$) of node $u$ on node $v$ [24]. By typing f.influence_graph(), the
graphical representation of this graph is displayed (see Row Out [3]). Then we
can compute all minimal and maximal trap spaces of the BN by typing
f.minimal_trapspaces() and f.maximal_trapspaces(), respectively. Rows Out [4]
and Out [5] show the tabular representations of the results, respectively. By
typing f.dynamics("asynchronous"), the STG of the BN under the asynchronous
update mode is obtained and displayed graphically (see Row Out [7]). Finally,
we check if state x reaches state y in the STG by typing f.reachability(x, y).
For the present STG, $000$ reaches $111$ and $010$ does not reach $100$.
Hence, the function returns True (see Row Out [8]) and False (see Row Out
[9]), respectively.

##  3 Conclusion

mpbn is distributed as a Python PyPi package (pip install mpbn) and conda
package (conda install -c colomoto -c potassco mpbn) under the BSD free
software license. It is also included in the CoLoMoTo Docker distribution [8].
Its source code is available at https://github.com/bnediction/mpbn together
with documentation and examples. Models and scripts used for the benchmarks
are provided at https://doi.org/10.5281/zenodo.10781704.

Combining a simple interface with state-of-the-art resolution algorithms, mpbn
is suited for all (1) Boolean model elementary analysis with state of-the-art
performance; (2) tool development, as a base (Python) library for implementing
advanced analysis, such as attractor analysis and control; and (3) teaching,
with interactive edition of BNs, analysis of their basic features, including
computation of STGs with different update modes. We believe that mpbn can
become a standard toolbox in the field of Boolean network research and has the
great potential to promote the study of mechanisms and control of biological
processes.

#### Acknowledgements

Work of L.P is supported by the French Agence Nationale pour la Recherche
(ANR) in the scope of the project “BNeDiction” (grant number
ANR-20-CE45-0001). Work of V-G.T is supported by Institute Carnot STAR,
Marseille, France.

## References

  * [1] Leon Glass and Stuart A Kauffman.  The logical analysis of continuous, non-linear biochemical control networks.  J. Theor. Biol., 39(1):103–129, 1973.
  * [2] René Thomas.  Boolean formalisation of genetic control circuits.  J. Theor. Biol., 42:565–583, 1973.
  * [3] Rui-Sheng Wang, Assieh Saadatpour, and Reka Albert.  Boolean modeling in systems biology: an overview of methodology and applications.  Phys. Biol., 9(5):055001, 2012.
  * [4] Christoph Müssel, Martin Hopfensitz, and Hans A. Kestler.  BoolNet - an R package for generation, reconstruction and analysis of Boolean networks.  Bioinform., 26(10):1378–1380, 2010.
  * [5] Claudine Chaouiya, Aurélien Naldi, and Denis Thieffry.  Logical modelling of gene regulatory networks with GINsim.  In Bacterial Molecular Networks, pages 463–479. Springer, 2012\.
  * [6] Tomás Helikar, Bryan M. Kowal, Sean McClenathan, et al.  The Cell Collective: Toward an open and collaborative approach to systems biology.  BMC Syst. Biol., 6:96, 2012.
  * [7] Hannes Klarner, Adam Streck, and Heike Siebert.  PyBoolNet: a python package for the generation, analysis and visualization of Boolean networks.  Bioinform., 33(5):770–772, 2017.
  * [8] Aurélien Naldi, Céline Hernandez, Nicolas Levy, et al.  The CoLoMoTo interactive notebook: accessible and reproducible computational analyses for qualitative biological networks.  Front. Physiol., 9:680, 2018.
  * [9] Loïc Paulevé, Juraj Kolčák, Thomas Chatain, et al.  Reconciling qualitative, abstract, and scalable modeling of biological networks.  Nat. Commun., 11(1):1–7, August 2020.
  * [10] Van-Giang Trinh, Belaid Benhamou, Kunihiko Hiraishi, et al.  Minimal trap spaces of logical models are maximal siphons of their Petri net encoding.  In International Conference on Computational Methods in Systems Biology, pages 158–176. Springer, 2022.
  * [11] Claudine Chaouiya, Duncan Bérenguier, Sarah M. Keating, et al.  SBML qualitative models: a model representation format and infrastructure to foster interactions between qualitative modelling formalisms and tools.  BMC Syst. Biol., 7(1):1–15, 2013.
  * [12] Léonard Hérault, Mathilde Poplineau, Estelle Duprez, et al.  A novel Boolean network inference strategy to model early hematopoiesis aging.  Comput. Struct. Biotechnol. J., 21:21–33, 2023.
  * [13] Clémence Réda and Andrée Delahaye-Duriez.  Prioritization of candidate genes through Boolean networks.  In International Conference on Computational Methods in Systems Biology, pages 89–121. Springer, 2022.
  * [14] Hannes Klarner, Alexander Bockmayr, and Heike Siebert.  Computing maximal and minimal trap spaces of Boolean networks.  Nat. Comput., 14(4):535–544, 2015.
  * [15] Kyungduk Moon, Kangbok Lee, and Loïc Paulevé.  Computational complexity of minimal trap spaces in Boolean networks, 2023.
  * [16] Jordan C. Rozum, Jorge Gómez Tejeda Zañudo, Xiao Gan, et al.  Parity and time reversal elucidate both decision-making in empirical models and attractor scaling in critical Boolean networks.  Sci. Adv., 7(29):eabf8124, July 2021.
  * [17] Van-Giang Trinh, Kunihiko Hiraishi, and Belaid Benhamou.  Computing attractors of large-scale asynchronous Boolean networks using minimal trap spaces.  In ACM International Conference on Bioinformatics, Computational Biology and Health Informatics, pages 13:1–13:10. ACM, 2022\.
  * [18] Laura Cifuentes Fontanals, Elisa Tonello, and Heike Siebert.  Control strategy identification via trap spaces in Boolean networks.  In International Conference on Computational Methods in Systems Biology, pages 159–175. Springer, 2020.
  * [19] Jordan C Rozum, Dávid Deritei, Kyu Hyong Park, et al.  pystablemotifs: Python library for attractor identification and control in Boolean networks.  Bioinform., 38(5):1465–1466, 2021.
  * [20] Martin Gebser, Benjamin Kaufmann, Roland Kaminski, et al.  Potassco: The Potsdam answer set solving collection.  AI Commun., 24(2):107–124, 2011.
  * [21] Samuel Pastva, David Safranek, Nikola Benes, et al.  Repository of logically consistent real-world Boolean network models.  bioRxiv, 2023.
  * [22] Nikola Benes, Lubos Brim, Samuel Pastva, et al.  Computing bottom SCCs symbolically using transition guided reduction.  In International Conference on Computer Aided Verification, pages 505–528. Springer, 2021.
  * [23] Van-Giang Trinh, Belaid Benhamou, Thomas Henzinger, et al.  Trap spaces of multi-valued networks: definition, computation, and applications.  Bioinf., 39(Supplement_1):i513–i522, 2023.
  * [24] Loïc Paulevé and Adrien Richard.  Static analysis of Boolean networks based on interaction graphs: a survey.  Electron. Notes Theor. Comput. Sci., 284:93–104, 2012.

Supplement

##  Appendix A Methods

In the tool mpbn, the computation of fixed points and minimal and maximal trap
spaces is performed by the means of Answer-Set Programming (ASP), a
declarative logic framework, and the solver clingo
DBLP:journals/aicom/GebserKKOSS11. Essentially, fixed point and trap space
identification problems are translated as logic satisfiability problems, where
each solution corresponds to a fixed point or trap space of the input Boolean
network. In this section, we detail a slightly simplified version of the ASP
encoding using in mpbn, and which extends the one presented in
DBLP:conf/ictai/ChevalierFPZ19 by adding support to non-monotone Boolean
functions, i.e., functions that depend both positively and negatively on a
same variable (e.g., exclusive-or functions).

###  A.1 Basic definitions

A _Boolean Network_ (BN) is specified by a function
$f\colon\mathbb{B}^{n}\to\mathbb{B}^{n}$, where $\mathbb{B}=\\{0,1\\}$ is the
Boolean domain. A Boolean function $f_{i}:\mathbb{B}^{n}\to\mathbb{B}$ is
_unate_ (or _monotone_) if, for each component $j\in\\{1,\cdots,n\\}$, one of
the two following properties holds:

  * •

for every vector $x\in\mathbb{B}^{n}$,

$f_{i}(x_{1},\cdots,x_{j-1},0,x_{j+1},\cdots,x_{n})\leq
f_{i}(x_{1},\cdots,x_{j-1},1,x_{j+1},\cdots,x_{n})$

  * •

for every vector $x\in\mathbb{B}^{n}$,

$f_{i}(x_{1},\cdots,x_{j-1},0,x_{j+1},\cdots,x_{n})\geq
f_{i}(x_{1},\cdots,x_{j-1},1,x_{j+1},\cdots,x_{n})$

If a Boolean function is not monotone, it is said non-monotone. E.g., the
function “$x\mapsto(x_{1}\wedge\neg x_{2})\vee(\neg x_{1}\wedge x_{2})$” is
non-monotone, whereas $x\mapsto\neg x_{1}\vee x_{2}$ is monotone. If, for each
$i\in\\{1,\cdots,n\\}$, the (local) function $f_{i}$ is monotone, then the BN
$f$ is said to be _locally-monotone_ ; otherwise, the BN $f$ is said non-
monotone.

A (sub)_cube_ is a set of Boolean vectors which is characterized by a vector
in $X\subseteq\\{0,1,\ast\\}^{n}$ and has vertices
$\\{x\in\mathbb{B}^{n}\mid\forall i\in\\{1,\cdots,n\\},X_{i}\neq\ast\implies
x_{i}=X_{i}\\}$. A cube $X$ is a _trap space_ for the BN $f$ if it is closed
by $f$, i.e., for each vertex $x\in X$ of the cube, $f(x)$ is also one of its
vertices.

In the scope of this supplement, a _Binary Decision Diagram_ (BDD) is a
directed acyclic graph with a single root node and two leaf nodes. Each leaf
node is associated to a value in $\mathbb{B}$ and each non-leaf node is
associated to a BN component in $\\{1,\cdots,n\\}$. Each non-leaf node has two
children, and every path from the root to a leaf traverses at most one node
associated to each BN component.

###  A.2 ASP encoding

We give a very brief overview of Answer-Set Programming (ASP) syntax and
semantics that we use in the next sections; see gekakasc12a for more details.

An ASP program is a Logic Program (LP) being a set of logical rules with first
order logic predicates of the form:

⬇

1$a_{0}$ $\leftarrow$ $a_{1}$, $\dots$, $a_{n}$, not $a_{n+1}$, $\dots$, not
$a_{n+k}$.

where $a_{i}$ are (variable-free) atoms, i.e., elements of the Herbrand base,
which is built from all the possible predicates of the LP. The Herbrand base
is built by instantiating the LP predicates with the LP terms (constants or
elements of the Herbrand universe).

Essentially, such a logical rule states that when all $a_{1},\dots,a_{n}$ are
true and none of $a_{n+1},\dots,a_{n+k}$ can be proven to be true, then
$a_{0}$ has to be true as well. Whenever $a_{0}$ is $\bot$ (false), the rule,
also called an _integrity constraint_ , becomes:

⬇

2$\leftarrow$$a_{1}$, $\dots$, $a_{n}$, not $a_{n+1}$, $\dots$, not $a_{n+k}$.

Such a rule is satisfied only if the right hand side of the rule is false (at
least one of $a_{1},\dots,a_{n}$ is false or at least one of
$a_{n+1},\dots,a_{n+k}$ is true). On the other hand, $a_{0}$ $\leftarrow$
$\top$ ($a_{0}$ is always true) is abbreviated as $a_{0}$.

Because our encoding does not involve default negation (not), a solution
(answer) is a subset-minimal Herbrand model (see
DBLP:journals/ngc/Przymusinski91), that is, a minimal set of true atoms where
all the logical rules are satisfied.

ASP allows using variables (starting with an upper-case) instead of
terms/predicates: these _template_ declarations will be expanded to the
corresponding propositional logic rules prior to the solving, in the
_grounding_ phase.

We also use the notations a((x;y)) which is expanded to a(x), a(y); $n$ {a(X):
b(X)} $m$ which is satisfied when at least $n$ and at most $m$ a(X) are true
where X ranges over the true b(X); and a(X): b(X) which is satisfied when for
each b(X) true, a(X) is true. If any term follows such a condition, it is
separated with ;. Finally, rules of form

⬇

2{a} $\leftarrow$ body.

leave the choice to make a true or not whenever the body is satisfied.

In the following, we assume fixing a BN
$f\colon\mathbb{B}^{n}\to\mathbb{B}^{n}$.

####  A.2.1 Encoding of Boolean functions

For each node $a$ of the BN, we declare an atom

⬇

2node($a$).

Let $\operatorname{DNF}[f_{a}]=C_{1}\vee\cdots\vee C_{k}$ be a Disjunctive
Normal Form (DNF) of $f_{a}$, where $C_{i}$ is a clause of the form
$C_{i}^{1}\wedge\cdots\wedge C_{i}^{l_{i}}$ ($l_{i}\geq 1$) where each literal
$C_{i}^{m},m\in\\{1,\dots,l_{i}\\}$ is either a node of the BN or the negation
of a node. We require that the DNF is well formed in the sense that no clause
subsumes another (i.e., there are no $C_{i}$, $C_{j}$, $i\neq j$ such that
$\\{C_{i}^{1},\cdots,C_{i}^{l_{i}}\\}\subseteq\\{C_{j}^{1},\cdots,C_{j}^{l_{j}}\\}$),
and there is no clause containing a literal and its negation. Whenever $k=0$,
i.e., $f_{a}$ has no clause, $f_{a}$ is the constant False function and is
declared in our encoding as

⬇

2constant($a$,-1).

Whenever $C_{1}=\emptyset$, i.e., $f_{a}$ has an empty clause, $f_{a}$ is the
constant True function and is declared in our encoding as:

⬇

2constant($a$,1).

Otherwise, for each clause $i\in\\{1,\cdots,k\\}$ and each
$m\in\\{1,\cdots,l_{i}\\}$, if the literal $C_{i}^{m}$ is positive, i.e., it
is a node $b$, it is declared as:

⬇

2clause($a$,$i$,$b$,1).

otherwise, i.e., it is the negation of a node $b$, it is declared as:

⬇

2clause($a$,$i$,$b$,-1).

If there is no node $b$ which appears both positively in one clause $C_{i}$
and negatively in another clause $C_{j}$, $f_{a}$ is unate (montone). Note
that this is only a sufficient condition. In that case, we add the atom

⬇

2unate($a$).

Otherwise, mpbn computes a reduced-ordered BDD representation of $f_{a}$ we
denote as $BDD_{a}$ and encode its graph representation. For each non-leaf
node $d$ of the BDD testing the BN component $b$ of the BN and having
respectively $d_{0}$ and $d_{1}$ as low and high children, we declare the
following atom:

⬇

2bdd($z$,$b$,($a$,$d_{0}$),($a$,$d_{1}$)).

where $z=a$ if $d$ is the root node, otherwise $z=(a,d)$. Finally, only the
leaf node $d$ for value False is declared:

⬇

2bdd(($z$,$d$),-1).

where $z$ is defined as above.

It is required that each path from the root to a leaf node of the BDD never
traverses two nodes testing a same BN component. This is the case for the BDDs
computed in mpbn by employing the pyeda Python
library111https://pyeda.readthedocs.io/en/latest/.

####  A.2.2 Encoding of Boolean function application

The following encoding ensures that, for a defined cube `X`, eval(X,N,-1)
(resp. eval(X,N,1)) is derived if and only if there exists a vertex in the
cube where the Boolean function of node `N` is False (resp. True).

The first case is whenever the Boolean function is constant:

⬇

2eval(X,N,V) $\leftarrow$ cube(X), node(N), constant(N,V).

Otherwise, the Boolean function is encoded as DNF using the atoms defined
above. We separated two cases: the evaluation to True, which is always
performed using the DNF, and the evaluation to False, which is performed using
the DNF representation only whenever the Boolean function is unate. Otherwise,
the evaluation to False is performed by the means of the BDD representation of
the Boolean function.

The evaluation from the DNF is performed as follows: evaldnf(X,N,C,1) is
derived if and only if each literal of the `C`-th clause is in the cube, i.e.,
there is one vertex in the cube for which the clause is satisfied. Similarly,
evaldnf(X,N,C,-1) is derived if and only if at least the _negation_ of one
literal `C`-th clause is in the cube, i.e., there is one vertex in the cube
for which the clause is not satisfied:

⬇

2evaldnf(X,N,C,1) $\leftarrow$ cube(X,M,V) : clause(X,M,V); cube(X),
clause(N,C,_,_).

3evaldnf(X,N,C,-1) $\leftarrow$ cube(X,M,-V), clause(N,C,M,V).

Then, eval(X,N,1) is derived whenever at least one of its clause has been
satisified. And, whenever the Boolean function is unate, eval(X,N,-1) is
derived if all the clause can be unsatisfied:

⬇

3eval(X,N,1) $\leftarrow$ evaldnf(X,N,C,1), clause(N,C,_,_).

4eval(X,N,-1) $\leftarrow$ evaldnf(X,N,C,-1) : clause(N,C,_,_); node(N),
cube(X), clause(N,_,_,_); unate(N).

Finally, whenever the BDD is present, i.e., whenever the Boolean function is
not unate, eval(X,N,-1) is derived if and only if there exists a path in the
BDD which matches with the cube and which leads to the negative (-1) leaf:

⬇

4eval(X,N,-1) $\leftarrow$ evalbdd(X,N,-1), node(N), cube(X).

5evalbdd(X,V,V) $\leftarrow$ cube(X), V=-1.

6evalbdd(X,B,V) $\leftarrow$ bdd(B,N,_,HI), cube(X,N,1), evalbdd(X,HI,V).

7evalbdd(X,B,V) $\leftarrow$ bdd(B,N,LO,_), cube(X,N,-1), evalbdd(X,LO,V).

8evalbdd(X,B,V) $\leftarrow$ cube(X), bdd(B,V), V=-1.

####  A.2.3 Encoding of fixed points

We take advantage of the genertic evaluation of Boolean functions over cubes
to encode the fixed point identification problem as follows: we declare a cube
`fb` which consists of a single vertex, together with an integrity constraint
which ensures that the evaluation of each Boolean function on that cube does
not lead to a different value:

⬇

4cube(fp).

51 { cube(fp,N,(-1;1)) } 1 $\leftarrow$ node(N).

6$\leftarrow$ cube(fp,N,V), eval(fp,N,-V).

The list of fixed points is then obtained by enumerating all the answer sets
projected to the atoms of the form cube(fp,N,V).

####  A.2.4 Encoding of trap spaces

Recall that trap spaces are cubes closed by Boolean functions. Therefore,
starting from a first non-empty cube `ts`, cube(ts,N,V) is derived whenever
eval(X,N,V) can be derived from the cube.

⬇

6cube(ts).

71 { cube(ts,N,(-1;1)) } $\leftarrow$ node(N).

8cube(ts,N,V) $\leftarrow$ eval(X,N,V).

Then the set of all trap spaces of the BN one-to-one corresponds to the set of
all answer sets projected over the atoms of the form of cube(ts,N,V). From
such an anwser set, one can reconstruct the associated trap space $X$ by
setting each node $a$ as free (i.e., $X_{a}=\ast$) whenver the answer set
contains both cube(ts,$a$,-1) and cube(ts,$a$,1), otherwise, it is fixed to
the correspondig value: $X_{a}=1$ (resp. $X_{a}=0$) if only cube(ts,$a$,1
(resp. cube(ts,$a$,-1)) is in the answer set.

The minimal and maximal trap spaces are then enumerated by exploiting the
domain heuristics of clingo which allows listing only the subset-minimal and
subset-maximal answer sets, corresponding exactly and respectively to minimal
and maximal trap spaces.

Note that in the case of maximal trap spaces, we need to add a cardinality
constraint to exclude from the solution space the trivial trap space
$\mathbb{B}^{n}$ where $n$ is the number of nodes of the BN:

⬇

8{ cube(ts,N,(-1;1)) : node(N) } $(2n-1)$.

Example. Let us consider the BN:

$\displaystyle f_{1}$ $\displaystyle=\neg x_{2}$ $\displaystyle f_{2}$
$\displaystyle=\neg x_{1}$ $\displaystyle f_{3}$
$\displaystyle=\neg(x_{1}\land\neg x_{2})\land\neg x_{3}$

We have that $\operatorname{DNF}[f_{1}]=\neg x_{2}$,
$\operatorname{DNF}[f_{2}]=\neg x_{1}$, and $\operatorname{DNF}[f_{3}]=(\neg
x_{1}\land\neg x_{3})\lor(x_{2}\land\neg x_{3})$. All the Boolean functions
are unate. Then the information about this BN is represented by the set of
rules as follows:

⬇

8unate(1).

9unate(2).

10unate(3).

11

12clause(1,1,2,0).

13clause(2,1,1,0).

14clause(3,1,1,0).

15clause(3,1,3,0).

16clause(3,2,2,1).

17clause(3,2,3,0).

Note that the rules for the Boolean function evaluation are fixed. The
characterizing rules are fixed for the cases of fixed points and minimal trap
spaces. For the case of maximal trap spaces, the cardinality constraint is not
fixed, it depends on the number of nodes of the BN. For the considered BN, it
is

⬇

8{ cube(ts,N,(-1;1)) : node(N) } 5.

We only consider answer sets projected over the atoms of the form of
cube(ts,N,V). Regarding fixed points, the respective ASP encoding has one
answer set {cube(ts, 1, 1), cube(ts, 2, -1), cube(ts, 3, -1)} that corresponds
to the fixed point 100 of the BN. Regarding minimal trap spaces, the
respective ASP encoding has two subset-minimal answer sets ({cube(ts, 1, -1),
cube(ts, 2, 1), cube(ts, 3, -1), cube(ts, 3, 1)} and {cube(ts, 1, 1), cube(ts,
2, -1), cube(ts, 3, -1)}) that correspond to two minimal trap spaces ($01\ast$
and $100$) of the BN, respectively. Regarding maximal trap spaces, the
respective ASP encoding has two subset-maximal answer sets ({cube(ts, 1, 1),
cube(ts, 2, -1), cube(ts, 3, -1), cube(ts, 3, 1)} and {cube(ts, 1, -1),
cube(ts, 2, 1), cube(ts, 3, -1), cube(ts, 3, 1)}) that correspond to two
maximal trap spaces ($10\ast$ and $01\ast$) of the BN, respectively.

##  Appendix B Experiments

To evaluate the efficiency of mpbn, we compared it with other state-of-the-art
methods regarding three prominent analysis problems on BNs: minimal trap space
enumeration, maximal trap space enumeration, and fixed point enumeration. For
each problem instance, we only measured the time to compute the first result,
which we believe to make the most fair comparison among the considered
methods. Since we tested a large number of both real-world and random models,
we set up a time limit of _one hour_ for each method on a problem instance.

All the compared tools are available as Python libraries. These libraries
along with all benchmark scripts and used data are available at
https://doi.org/10.5281/zenodo.10781704. All experiments were performed using
a desktop computer running Linux on an Intel(R) Xeon(R) Gold 6244 CPU at
3.60GHz. We ran the experiments sequentially and in general only used a single
core, limited to 32GB of RAM. The running time was measured internally by each
experiment script (i.e., it did not count the overhead of starting the Python
interpreter). However, it included the time for all steps of the computation.

###  B.1 Tested tools

We tested a variety of tools that support the enumeration of trap spaces and
fixed points in BNs. For each tool, we used its best method for a specific
problem type. Regarding mpbn, we considered two “milestone” versions where
mpbn 1.6 is the version described in the original paper Paulev2020, and mpbn
3.3 is the latest version that provides many new methodological materials (see
Section A), especially the ability for handling non-monotone BNs, which was
not the case for mpbn 1.6.

Table 2 summarizes the existing tools of which we are aware and their
supported features for BN analysis. Regarding the minimal trap space
enumeration, we omitted trappist because trapmvn is its successor. trapmvn
iterates on trappist by adding heuristics to improve the Petri net encoding
process. We also omitted biolqm naldi2018biolqm that relies on BDDs because it
always requires to compute all results, in contrast to other ASP-based
methods. Moreover, due to the inherent drawbacks of both BDDs and the method
itself, biolqm is not expected to handle BNs with large size and complex
update functions Trinh2023tcs. With the same reasons, we omitted biolqm for
the maximal trap space enumeration and the fixed point enumeration. Note
however that there are three other notable tools that only support the fixed
point enumeration: an-asp DBLP:journals/almob/AbdallahFRM17, bns
DBLP:journals/tcbb/DubrovaT11, and fpcollector
DBLP:journals/bioinformatics/AracenaCS21. The approaches of an-asp and trapmvn
are similar as they rely on the transition-based representations of the
original BN, and the constructions both rely on the computation of DNFs of
Boolean functions. In addition, it has been shown in trinh2023trap that
trapmvn is comparable to an-asp, even better on average. bns only supports
enumerating all fixed points, and it is limited by the complexity of update
functions. Indeed, it only handles Boolean functions with less than 20 input
variables. When exceeding this bound, it does not compute anything. Similarly,
fpcollector only supports enumerating all fixed points and it is indeed not
expected to handle large and complex BNs. Hence, we omitted an-asp, bns, and
fpcollector for the fixed point enumeration. Overall, we have four tested
tools for each of the three problem types: mpbn 1.6, mpbn 3.3, pyboolnet, and
trapmvn. It is worth noting that to our best knowledge pyboolnet and trapmvn
are the most recent and efficient methods for such kinds of analysis on BNs,
which is justified by the extensive experiments conducted by
klarner2015computing,Trinh2023tcs,trinh2023trap.

Table 2: Summary of existing tools and their supported features for BN analysis. Columns 2-4 indicate the minimal trap space enumeration, the maximal trap space enumeration, and the fixed point enumeration, respectively. Tool |  Minimal |  Maximal |  Fixed point
---|---|---|---
mpbn |  yes |  yes |  yes
pyboolnet klarner2017pyboolnet |  yes |  yes |  yes
trappist DBLP:conf/cmsb/TrinhBHS22,Trinh2023tcs |  yes |  no |  no
trapmvn trinh2023trap |  yes |  yes |  yes
biolqm naldi2018biolqm |  yes |  yes |  yes
an-asp DBLP:journals/almob/AbdallahFRM17 |  no |  no |  yes
bns DBLP:journals/tcbb/DubrovaT11 |  no |  no |  yes
fpcollector DBLP:journals/bioinformatics/AracenaCS21 |  no |  no |  yes

###  B.2 Tested models

We tested the tools on a wide range of real-world and random models. In
particular, we used:

##### Biodivine Boolean Models (BBM)

The BBM repository pastva2023repository provides a wide variety of published
_biologically relevant_ BN models. Here, we used the August 2022
edition222https://github.com/sybila/biodivine-boolean-
models/releases/tag/august-2022 that consists of 212 models, ranging up to 321
variables and 1100 regulations.

##### Manually selected models

To supplement the BBM dataset, we also performed a separate survey of related
literature and found 23 additional _biologically relevant_ models. These
models are non-trivial, even contain a very large number of nodes. A summary
of these models, ranging up to 4691 variables, is given in Table 3.

##### Very Large Boolean Networks (VLBN)

The VLBN dataset333https://doi.org/10.5281/zenodo.3714875 provides 28 _random_
BNs with scale-free topology and inhibitor-dominant update functions
Paulev2020. The models range up to 100.000 variables. They are very large, but
have rather simple non-monotone update functions.

##### Manually generated models

To supplement the VLBN dataset, we also used a dataset (namely AEON) of 100
_random_ BNs generated by the generator of DBLP:conf/cav/BenesBPS21, ranging
up to 1016 variables. This generator uses a degree distribution based on the
BBM dataset to sample the network topology. For update functions, it samples
from a subset of nested-canalizing unate functions. Compared to the VLBN
dataset, it thus covers a smaller range of sizes, but a wider range of update
functions.

Table 3: Selected real-world models. The table lists total variable count $n$, the number of source (i.e., input) variables $s$, and the respective bibliographic reference. No. | Filename | $n$ | $s$ | Source
---|---|---|---|---
1 | Rho-family_GTPases_signaling | 33 | 1 |  DesignPrinciplesGeneNetworks
2 | tca_cycle | 69 | 35 |  hemedan2023applications
3 | Executable_..._mast_cell_..._BCC | 73 | 19 |  aghamiri2020automated
4 | Leukaemia.free-inputs | 107 | 6 |  trinh2023trap
5 | EMT_Mechanosensing | 136 | 4 |  Sullivan2022
6 | angiofull | 142 | 28 |  Weinstein2017
7 | EMT_Mechanosensing_TGFbeta | 150 | 6 |  Sullivan2022
8 | VPC.free-inputs | 169 | 7 |  trinh2023trap
9 | InVivo.free-inputs | 179 | 7 |  trinh2023trap
10 | Executable_..._MAPK_model_BCC | 181 | 37 |  aghamiri2020automated
11 | InVitro.free-inputs | 185 | 9 |  trinh2023trap
12 | T-cell_co-receptor_molecules_calcium_channel | 206 | 39 |  Ganguli2015
13 | SkinModel.free-inputs | 300 | 10 |  trinh2023trap
14 | Leishmania | 342 | 81 |  DBLP:journals/ejbsb/GanguliCCS15
15 | Metabolism_demo.free-inputs | 355 | 9 |  trinh2023trap
16 | Executable_file_for_cholocystokinin_model_BCC | 383 | 74 |  aghamiri2020automated
17 | ra_map | 447 | 125 |  Singh2023
18 | CAF-model | 463 | 62 |  Aghakhani2023.05.11.540378
19 | Executable_file_for_Alzheimer_model_BCC | 762 | 237 |  aghamiri2020automated
20 | S1_Table | 1659 | 521 |  DBLP:conf/cmsb/TrinhBHS22
21 | Human_network | 1953 | 669 |  DBLP:conf/cmsb/TrinhBHS22
22 | SN5 | 2746 | 829 |  DBLP:conf/cmsb/TrinhBHS22
23 | turei_2016 | 4691 | 1257 |  DBLP:conf/cmsb/TrinhBHS22

###  B.3 Results on minimal trap spaces

Regarding the minimal trap space enumeration, Table 4 summarizes the obtained
results. We here reported the number of models completed within a specific
time limit for each tool on each dataset. To better visualize the performance
scaling of individual tools on the real-world and random models, we prepared
Figures 2 and 3, respectively. These figures show in detail how many models
can be completed by each tool within a specific time limit. There are 235
models come from the BBM repository and the selected models and 128 random
models come from the VLBN and AEON datasets.

Table 4: Summary of tool performance when computing the first minimal trap
space. Columns 2-7 give the number of models completed within the respective
time limit. 212 BBM models
---
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 141 | 166 | 187 | 190 | 200 | 200
trapmvn | 206 | 208 | 211 | 211 | 211 | 211
mpbn 1.6 | 99 | 99 | 99 | 99 | 99 | 99
mpbn 3.3 | 207 | 211 | 212 | 212 | 212 | 212
23 selected models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 4 | 5 | 5 | 8 | 12 | 14
trapmvn | 14 | 15 | 16 | 22 | 23 | 23
mpbn 1.6 | 5 | 8 | 9 | 9 | 9 | 9
mpbn 3.3 | 15 | 20 | 23 | 23 | 23 | 23
28 VLBN models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 0 | 7 | 8 | 14 | 20
mpbn 1.6 | 1 | 7 | 15 | 20 | 28 | 28
mpbn 3.3 | 4 | 8 | 16 | 20 | 28 | 28
100 AEON models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 6 | 47 | 96 | 100 | 100
mpbn 1.6 | 100 | 100 | 100 | 100 | 100 | 100
mpbn 3.3 | 100 | 100 | 100 | 100 | 100 | 100

0.5s2s10s1min10min1h$99$$150$$200$$250$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 2: Cumulative minimal trap space experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 235 real-world models.

0.5s2s10s1min10min1h$0$$25$$50$$75$$100$$130$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 3: Cumulative minimal trap space experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 128 randomly generated
models.

For real-world models, we first observed that mpbn 3.3 completely overcomes
the limitation on non-monotone BNs of mpbn 1.6. mpbn 3.3 completed much more
models than mpbn 1.6 for every time limit and all such extra models are non-
monotone. This result confirms the efficacy of the new methedological
materials that we proposed and implemented in mpbn 3.3. Second, we can see
that mpbn 3.3 is the fastest tool as it completed more models than all the
other tools for every time limit. In particular, it is the sole tool that can
handle all the BBM models with the time limit 1h. Actually, it completed every
BBM model (also selected model) within 10s. Third, although mpbn 3.3 is better
than pyboolnet and trapmvn, their performance differences are not much
exhibited. This can be explained by the fact that in most of the real-world
models, update functions have quite simple forms, even sometimes just simple
conjunctions or disjunctions of literals.

For random models, the performance difference between mpbn 1.6 and mpbn 3.3 is
negligible because all the considered random models are locally-monotone.
Second, pyboolnet could not handle any random model. It is not surprising
because these models have complex update functions, which is the main weakness
of the ASP encoding based on prime implicants Trinh2023tcs. Third, trapmvn
completed all the AEON models with the time limit of 10min, but it completed
only 20 VLBN models (it failed with all 50.000-node and 100.000-node models)
with the time limit of 1h. The reason is that for random models, the number of
transitions of the Petri net encoding is large, making the ASP encoding more
complicated. Moreover, for the majority of the succeeded models, it took more
than 10s each. Finally, mpbn 3.3 vastly outperforms trapmvn. It completed much
more models than trapmvn for every time limit in the case of VLBN models and
for all time limits of at most 10s in the case of AEON models. In particular,
it is the sole tool that can handle all VLBN models with the time limit of 1h
(actually it can handle every such model within 10min) and it can handle every
AEON model within only 0.5s.

###  B.4 Results on maximal trap spaces

Regarding the maximal trap space enumeration, the results are presented in
Table 5 and Figures 4 and 5. These results do not reveal any conclusions that
are not covered by the minimal trap space case.

Table 5: Summary of tool performance when computing the first maximal trap
space. Columns 2-7 give the number of models completed within the respective
time limit. 212 BBM models
---
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 140 | 166 | 188 | 190 | 200 | 200
trapmvn | 206 | 208 | 211 | 211 | 211 | 211
mpbn 1.6 | 99 | 99 | 99 | 99 | 99 | 99
mpbn 3.3 | 207 | 211 | 212 | 212 | 212 | 212
23 selected models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 4 | 5 | 5 | 8 | 12 | 14
trapmvn | 14 | 15 | 16 | 22 | 23 | 23
mpbn 1.6 | 5 | 8 | 9 | 9 | 9 | 9
mpbn 3.3 | 15 | 19 | 23 | 23 | 23 | 23
28 VLBN models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 0 | 7 | 10 | 16 | 16
mpbn 1.6 | 1 | 8 | 15 | 20 | 28 | 28
mpbn 3.3 | 4 | 8 | 16 | 23 | 28 | 28
100 AEON models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 7 | 52 | 96 | 100 | 100
mpbn 1.6 | 100 | 100 | 100 | 100 | 100 | 100
mpbn 3.3 | 100 | 100 | 100 | 100 | 100 | 100

0.5s2s10s1min10min1h$99$$150$$200$$250$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 4: Cumulative maximal trap space experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 235 real-world models.

0.5s2s10s1min10min1h$0$$25$$50$$75$$100$$130$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 5: Cumulative maximal trap space experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 128 randomly generated
models.

###  B.5 Results on fixed points

Regarding the fixed point enumeration, the results are presented in Table 6
and Figures 6 and 7. These results do not reveal any conclusions that are not
covered by the minimal trap space case.

Table 6: Summary of tool performance when computing the first fixed point.
Columns 2-7 give the number of models completed within the respective time
limit. 212 BBM models
---
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 139 | 162 | 185 | 189 | 199 | 199
trapmvn | 207 | 209 | 211 | 211 | 211 | 211
mpbn 1.6 | 99 | 99 | 99 | 99 | 99 | 99
mpbn 3.3 | 209 | 211 | 212 | 212 | 212 | 212
23 selected models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 3 | 5 | 5 | 8 | 11 | 13
trapmvn | 15 | 15 | 16 | 23 | 23 | 23
mpbn 1.6 | 5 | 8 | 9 | 9 | 9 | 9
mpbn 3.3 | 15 | 19 | 23 | 23 | 23 | 23
28 VLBN models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 0 | 7 | 12 | 18 | 22
mpbn 1.6 | 1 | 5 | 10 | 16 | 20 | 20
mpbn 3.3 | 4 | 8 | 12 | 16 | 24 | 28
100 AEON models
Method | <0.5s | <2s | <10s | <1min | <10min | <1h
pyboolnet | 0 | 0 | 0 | 0 | 0 | 0
trapmvn | 0 | 14 | 56 | 96 | 100 | 100
mpbn 1.6 | 99 | 100 | 100 | 100 | 100 | 100
mpbn 3.3 | 100 | 100 | 100 | 100 | 100 | 100

0.5s2s10s1min10min1h$99$$150$$200$$250$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 6: Cumulative fixed point experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 235 real-world models.

0.5s2s10s1min10min1h$0$$25$$50$$75$$100$$130$Runtime (log)Completed instances

pyboolnet $\blacksquare$ / trapmvn $\blacksquare$ / mpbn 1.6 $\blacksquare$ /
mpbn 3.3 $\blacksquare$

Figure 7: Cumulative fixed point experiments completed (y-axis) until a
specific time point (x-axis, logarithmic). Concerns the 128 randomly generated
models.

unsrt ref