11institutetext:  Aix-Marseille Univ., Toulon Univ., CNRS, LIS, Marseille,
France

# A framework for (de)composing with Boolean automata networks

Kévin Perrot 11 Pacôme Perrotin Corresponding author: pacome.perrotin@lis-
lab.fr.11 Sylvain Sené 11

###### Abstract

Boolean automata networks (BANs) are a generalisation of Boolean cellular
automata. In such, any theorem describing the way BANs compute information is
a strong tool that can be applied to a wide range of models of computation. In
this paper we explore a way of working with BANs which involves adding
external inputs to the base model (via modules), and more importantly, a way
to link networks together using the above mentioned inputs (via wirings). Our
aim is to develop a powerful formalism for BAN (de)composition. We formulate
two results: the first one shows that our modules/wirings definition is
complete; the second one uses modules/wirings to prove simulation results
amongst BANs.

###### Keywords:

B

oolean automata networks, modules, wirings, simulation.

##  1 Introduction

Boolean automata networks (BANs) can be seen as a generalisation of cellular
automata that enables the creation of systems composed of Boolean functions
over any graph, while cellular automata only operate over lattices of any
dimension. The study of the dynamics of a BAN, that describes the set of all
computations possible in such a system, is a wide and complex subject. From
very simple networks computing simple Boolean functions to possibly infinite
networks able to simulate any Turing machine, the number of configurations
always grows exponentially with the size of the network, making any exhaustive
examination of its dynamics impractical. The study of such dynamics is
nevertheless an important topic which can impact other fields. BANs are for
example used in the study of the dynamics of gene regulatory networks [8, 12,
17] in biology.

Many efforts to characterise the dynamics of BANs have already been put
forward. For example, some studies [1, 14] examine the behaviour of networks
composed of interconnected cycles. The modularity of BANs has been studied
from multiple perspectives. In particular from a static point of view [2, 13],
and a functional one [4, 7, 16]. In this paper, we explore a compositional
approach to BANs that allows to decompose a BAN into subnetworks called
modules, and to compose modules together in order to form larger networks. We
define a module as a BAN on which we add external inputs. These inputs are
used to manipulate the result of the network computation by adding extra
information. They can also be used to interconnect multiple modules, making
more complex networks. Those constructions resemble the circuits described in
Feder’s thesis [9], and modules can be seen as a generalisation of circuits
over any update mode.

Section 2 discusses the possible motivations for a (de)compositional study of
BANs. Section 3 introduces BANs and update modes, and Sections 4 and 5 develop
a formalism for the modular study of BANs, justified by a first theorem
showing that any network can be created with modules and wirings. We also
present an application of our definitions to BAN simulation in Section 6,
leading to a second theorem stating that composing with local simulations is
sufficient to (globally) simulate a BAN. Finally, Section 7 presents and
analyses two illustrations of the principles presented in Section 2.

The demonstrations of all results are given in appendix.

##  2 Motivations

BANs, despite being very simply defined locally, become complex to analyse as
the representation of their dynamics grows exponentially in the size of their
networks. BANs have been proven to be Turing-complete [5] and as most of
Turing-complete systems are able to show complex and emergent properties.

Yet, an important number of networks can be partially understood when viewed
through the lens of functionality (what an object is meant to achieve).
Functionality enables to use abstraction to reduce the considered network (or
some part of it) to the computation of a function or the simulation of a
dynamical system. Assuming a functionality of the parts of a network can let
us conclude on the functionality of the network itself, at the cost of letting
aside an absolute characterisation of its dynamics (which is often practically
impossible). Such a functional interpretation aims at offering the possibility
to make verifiable predictions in a short amount of time.

It is not known if every Boolean automata network can be cut into a reasonable
amount of parts to which one can easily affect a functionality. We will
justify our present argument by illustrating it in Section 7.

##  3 Boolean automata networks

###  3.1 Preliminary notations

Let us first describe some of the notations used throughout the paper. Let
$f:A\to B$ be a mapping from set $A$ to set $B$. For $S\subseteq A$ we denote
$f(S)=\\{b\in B\mid\exists a\in S,f(a)=b\\}$. We denote $f\bigl{\lvert}_{S}$
the restriction of $f$ to the domain $S$, $f\bigl{\lvert}_{S}:S\to B$ such
that $f\bigl{\lvert}_{S}(a)=f(a)$ for all $a\in S$. Let $\mathrm{dom}(f)$ be
the domain of $f$, and $g\circ f$ the composition of $f$ then $g$. For $f$ and
$g$ two functions with disjoint domains of definition, we define $f\sqcup g$
as the function defined such that :

$f\sqcup g(x)=\begin{array}[]{\\{}{ll}.f(x)&\text{ if
}x\in\mathrm{dom}(f)\\\\[5.0pt] g(x)&\text{ if
}x\in\mathrm{dom}(h)\end{array}\text{.}$

We denote $\mathbb{B}=\\{0,1\\}$ the set of Booleans. For $K$ a sequence of
$m$ elements, the sub-sequence from the $i$-th element to the $j$-th element
is denoted $K_{[i,j]}$. We sometimes define functions without naming them with
the notation $a\mapsto b$, signifying that for any input $a$ the function will
return $b$. For example, the function $n\mapsto 2\times n$ is a function that
takes a number $n$ and returns the value of $n$ multiplied by $2$.

###  3.2 Definitions

A BAN is based upon a set of automata. Each automaton is defined as a Boolean
function, with arity the size of the network. Each variable of the function of
each automaton is meant to correspond to an automaton in the network. By
considering a configuration of Boolean values over this network, we can
compute the Boolean function of each automaton and obtain a Boolean value for
each automaton (_i.e._ a local state). These values can be used to update the
global state of the network, that we call a configuration. If we decide to
update the value of each automaton at once, the update mode is parallel.
However, if only one automaton is updated at each time step, the update mode
is sequential [10, 15].

###### Definition 1

A _configuration_ on a set $S$ is a function $x:S\to\mathbb{B}$.

A BAN $F$ defined over the set $S$ associates a Boolean function to each
element of $S$. Each of theses functions is defined from the set of all
configurations of the BAN, $S\to\mathbb{B}$, to the Boolean set, $\mathbb{B}$.

###### Definition 2

For $S$ a set, a _Boolean automata network_ (BAN) $F$ is a function
$F:S\to(S\to\mathbb{B})\to\mathbb{B}$.

For each $s\in S$, we denote $f_{s}=F(s)$ the local function of automaton $s$.

For $s\in S$ we denote $x_{s}=x(s)$. A function $x$ is a configuration at a
given time over the network. Thus, we can define our function $f_{s}$ to be
part of the set $(S\to\mathbb{B})\to\mathbb{B}$. This way, a BAN $F$ can be
defined as a function from the set $S$ to the set
$(S\to\mathbb{B})\to\mathbb{B}$. We find again that the set of all BANs over
$S$ can simply be defined as $S\to(S\to\mathbb{B})\to\mathbb{B}$. For any BAN
$F$ and configuration $x$, we can define the configuration which is computed
by $F$ from $x$. A naive way to do so would be to define $x^{\prime}=F(x)$
such that $x^{\prime}_{s}=f_{s}(x)$ for every $s$; this definition however is
very limiting: it only allows parallel updates of our system. In a general
definition of BANs, a computation of a BAN should allow updates of only a
subset of the functions of the network. Slight changes to the update mode of a
BAN can deeply change its computational capabilities [3, 11]. Most results
that assume a parallel update mode cannot be applied to a sequential network;
the reciprocal is also true. We set the following definition of an update over
our BAN to be as general as possible.

###### Definition 3

Any $\delta\subseteq S$ is an _update_ over $S$.

One can apply multiple consecutive updates to a BAN to effectively execute the
BAN over an update mode. An _update mode_ is simply a sequence of updates that
is denoted $\Delta$, where $\Delta_{k}$ is the $k^{\text{th}}$ update of the
sequence. We define the union operator between updates modes as it will be
useful for the proof of our last theorem.

###### Definition 4

Let $\Delta$, $\Delta^{\prime}$ be two update modes over a set $S$. The
_union_ of $\Delta$ and $\Delta^{\prime}$ denoted $\Delta\cup\Delta^{\prime}$
is the update mode defined as
$(\Delta\cup\Delta^{\prime})_{k}=\Delta_{k}\cup\Delta^{\prime}_{k}$. The size
of $\Delta\cup\Delta^{\prime}$ is the maximum among the sizes of $\Delta$ and
$\Delta^{\prime}$.

We assume that $\Delta_{k}=\varnothing$ if $k$ is greater than the size of
$\Delta$. Given an update $\delta$, we can define the endomorphism
$F_{\delta}$ over the set of all configurations. For every configuration $x$,
we set $F_{\delta}(x)(s)=f_{s}(x)$ if $s\in\delta$, and
$F_{\delta}(x)(s)=x(s)$ if $s\notin\delta$. In other words, the value of $s$
in the new configuration is set to $f_{s}(x)$ only if $s\in\delta$, otherwise
the Boolean affectation of $s$ remains $x_{s}$. Now, we can define the
execution of $F$ in a recursive way.

###### Definition 5

The _execution_ of $F$ over $x$, under the update mode $\Delta$, is the
function $F_{\Delta}:(S\to\mathbb{B})\to(S \to\mathbb{B})$ defined as
$F_{\Delta[1,k]}(x)=F_{\Delta_{k}}(F_{\Delta[1,k-1]}(x))$, with
$F_{\Delta[1,1]}(x)=F_{\Delta_{1}}(x)$.

Throughout this paper we represent BANs as graphs called interaction graphs.
Interaction graphs are a classical tool in the study of BANs. For a BAN $F$
defined over $S$, the interaction graph of $F$ is the oriented graph
$G=(S,\epsilon)$, where $(s,s^{\prime})\in\epsilon$ if and only if the
variable $x_{s}$ influences the computation of the function $F(s^{\prime})$.

##  4 Modules

Modules are BANs with external inputs. Such inputs can be added to any local
function of a module, and any local function of a module can have multiple
inputs. When a local function has $n$ inputs, the arity of this function is
increased by $n$. These new parameters are referred to by elements in a new
set $E$: the elements of $E$ describe the inputs of the module; those of $S$
describe the internal elements of the module. To declare which input $e\in E$
is affected to each function $f_{s}$, we use function $\alpha$.

###### Definition 6

Let $S$ and $E$ be two disjoint sets. An _input declaration_ over $S$ and $E$
is a function $\alpha:S\rightarrow\mathcal{P}(E)$ such that $\\{\alpha(s)\mid
s\in S\\}$ is a partition of $E$.

For each $s$, $\alpha(s)$ is the set of all external inputs of function
$f_{s}$. The partition property is important because without it, some input
could be assigned to multiple nodes, or to no node at all, which is contrary
to our vision of input. To simplify notations, we sometimes denote
$E_{s}=\alpha(s)$. Now, let us explicit the concept of a module.

###### Definition 7

A _module_ $M$ over $(S,E,\alpha)$ is defined such that, for each $s\in S$,
$M(s)$ is a function $M(s):(S\cup E_{s})\to\mathbb{B}$.

If $M$ is a module defined over $(S,\varnothing,s\mapsto\varnothing)$, $M$ is
also a BAN. To compute anything over this new system, we need a configuration
$x:S\to\mathbb{B}$ and a configuration over the elements of $E$.

###### Definition 8

An _input configuration_ over $E$ is a function $i:E\to\mathbb{B}$.

Let $x$ be a configuration over $S$, and $i$ an input configuration over $E$.
As $x$ and $i$ are defined over disjoint sets, we define $x\sqcup i$ as their
union. Such an union, coupled with an update over $S$, is enough information
to perform a computation over this new model.

###### Definition 9

Let $x$ be a configuration over $S$ and $i$ an input over $E$. Let $\delta$ be
an update over $S$. The _computation_ of $M$ over $x$, $i$ and $\delta$,
denoted $M_{\delta}(x\sqcup i)$, is the configuration over $S$ such that
$M_{\delta}(x\sqcup i)(s)=f_{s}(x\sqcup i\bigl{\lvert}_{E_{s}})$ for each
$s\in\delta$, and $M_{\delta}(x\sqcup i)(s)=x(s)$ for every $s\in
S\setminus\delta$.

In the following example, we assume a total order over $S\cup E$, allowing us
to intuitively write configurations as binary words. For example, $x=101$
means $x(a)=1$, $x(b)=0$ and $x(c)=1$.

abc$a_{1}$$a_{2}$$a_{3}$$b_{1}$$b_{2}$$c_{1}$ Figure 1: Interaction graph of
the module detailed in Example 1.

###### Example 1

$S=\\{a,b,c\\}$, and $E=\\{a_{1},a_{2},a_{3},b_{1},b_{2},c_{1}\\}$. We define
$\alpha$ such that $\alpha(a)=\\{a_{1},a_{2},a_{3}\\}$,
$\alpha(b)=\\{b_{1},b_{2}\\}$ and $\alpha(c)=\\{c_{1}\\}$. Let $M$ be a module
over $(S,E,\alpha)$, such that $M(a)=x_{b}\vee a_{1}\vee a_{2}\vee a_{3}$,
$M(b)=\neg x_{b}\vee x_{c}\vee\neg b_{1}\wedge b_{2}$, and $M(c)=\neg c_{1}$.
Let $x=101$, $i=000010$ and $\delta=\\{a,b\\}$. We get that
$M_{\delta}(x\sqcup i)=M_{\\{a,b\\}}(101\sqcup 000010)$ is such that
$M_{\delta}(x\sqcup i)(a)=f_{a}(x\sqcup i\bigl{\lvert}_{E_{a}})=0$,
$M_{\delta}(x\sqcup i)(b)=f_{b}(x\sqcup i\bigl{\lvert}_{E_{b}})=1$, and
$M_{\delta}(x\sqcup i)(c)=x(c)=1$. Therefore $M_{\delta}(x\sqcup i)=011$. A
representation of this module is pictured in Figure 1.

Let us now define executions, while considering that the input configuration
can change over time.

###### Definition 10

Let $t>1$. Let $I=(i_{1},i_{2},\ldots,i_{t-1})$ be a sequence of input
configurations over $E$, $X=(x_{1},x_{2},\ldots,x_{t})$ a sequence of
configurations over $S$, and $\Delta$ an update mode over $S$ of size $t$.
$(X,I,\Delta)$ is an _execution_ of $M$ if for all $1\leq k<t$,
$x_{k+1}=M_{\Delta_{k}}(x_{k}\cup i_{k})$.

This definition allows for variation over the inputs over time. As this
particular feature is not needed throughout this paper, we also propose a
simpler definition of executions over modules which only allows fixed input
values over time.

###### Definition 11

Let $i$ be an input configuration over $E$. The _execution_ of $M$ over $x\cup
i$ with update mode $\Delta$ is an endomorphism over the set of all
configurations, denoted $M_{\Delta}$. It is defined as
$M_{\Delta[1,k]}(x\sqcup i)=M_{\Delta_{k}}(M_{\Delta[1,k-1]}(x\sqcup i)\sqcup
i)$, with $M_{\Delta[1,1]}(x\sqcup i)=M_{\Delta_{1}}(x\sqcup i)$.

##  5 Wirings

The external inputs of a module can be used to encode any information. For
instance, we could encode any periodic (or non-periodic) sequence of Boolean
words into the inputs of a given module. We could also encode the output of a
given BAN or module, combining in some way the computational power of both
networks. Such a composition of modules is captured by our definition of
wirings. A wiring is an operation that links together different inputs and
automata from one more or modules, thus forming bigger and more complex
modules.

We decompose this compositional process into two different families of
operators: the non-recursive and the recursive wirings. The first ones connect
the automata of one module to the inputs of another; the second ones connect
the automata of a module to its own inputs. A wiring, recursive or not, is
defined by a partial map $\omega$ linking some inputs to automata. Let us
first define non-recursive wirings.

###### Definition 12

Let $M$, $M^{\prime}$ be modules defined over $(S,E,\alpha)$ and
$(S^{\prime},E^{\prime},\alpha^{\prime})$ respectively, such that
$S,S^{\prime}$ and $E,E^{\prime}$ are two by two disjoint. A _non-recursive
wiring_ from $M$ to $M^{\prime}$ is a partial map $\omega$ from $E^{\prime}$
to $S$.

The new module result of the non-recursive wiring $\omega$ is denoted
$M\rightarrowtail_{\omega}M^{\prime}$ and is defined over $(S\cup
S^{\prime},E\cup E^{\prime}\setminus\mathrm{dom}(\omega),\alpha_{\omega})$.
The input declaration of $M\rightarrowtail_{\omega}M^{\prime}$ is
$\alpha_{\omega}(s)=\alpha(s)\setminus\mathrm{dom}(\omega)$ (in particular,
$\alpha_{\omega}(s)=\alpha(s)$ if $s\in S$). Given $s\in S\cup S^{\prime}$,
the local function $M\rightarrowtail_{\omega}M^{\prime}(s)$, denoted
$f^{\omega}_{s}$, is defined as

$f^{\omega}_{s}(x\sqcup
i)=\begin{array}[]{\\{}{ll}.f_{s}(x\bigl{\lvert}_{S}\sqcup
i\bigl{\lvert}_{E_{s}})&\text{ if }s\in S\\\\[5.0pt]
f^{\prime}_{s}(x\bigl{\lvert}_{S^{\prime}}\sqcup
i\bigl{\lvert}_{E^{\prime}_{s}\setminus\mathrm{dom}(\omega)}\sqcup(x\circ\omega\bigl{\lvert}_{E^{\prime}_{s}}))&\text{
if }s\in S^{\prime}\end{array}\text{.}$

In this new module, some inputs of $M^{\prime}$ have been assigned to the
values of some elements of $M$. Such assignments are defined in the wiring
$\omega$. For any $s\in S\cup S^{\prime}$, the function
$M\rightarrowtail_{\omega}M^{\prime}(s)$ (denoted $f^{\omega}_{s}$) is defined
over $(S\cup S^{\prime}\cup\alpha_{\omega}(s))\to\mathbb{B}$. In the case
$s\in S^{\prime}$, the image of $x\sqcup i$ is given by $f^{\prime}_{s}$ which
expects a configuration on $S^{\prime}\cup E^{\prime}_{s}$: the configuration
on $S^{\prime}$ is provided by $x$, and the configuration on $E^{\prime}$ is
partly provided by $i$ (on $E^{\prime}_{s}\setminus\mathrm{dom}(\omega)$), and
partly provided by $(x\circ\omega)$ (on $\mathrm{dom}(\omega)\cap
E^{\prime}_{s}$).

###### Definition 13

Let $M$ be a module over $(S,E)$. A _recursive wiring_ of $M$ is a partial map
$\omega$ from $E$ to $S$.

With $\omega$ defining now a recursive wiring over a module $M$, the result is
similar if not simpler than in the definition of non-recursive wirings. The
new module obtained from a recursive wiring $\omega$ on $M$ is denoted
$\circlearrowright_{\omega}M$ and is defined over
$(S,E\setminus\mathrm{dom}(\omega),\alpha_{\omega})$ with the input
declaration defined as, for any $s\in S$,
$\alpha_{\omega}(s)=\alpha(s)\setminus\mathrm{dom}(\omega)$. Given $s\in S$,
$x$ and $i$, the local function $\circlearrowright_{\omega}M(s)$ is denoted
$f^{\omega}_{s}$ and is evaluated to $f^{\omega}_{s}(x\sqcup i)=f_{s}(x\sqcup
i\bigl{\lvert}_{E_{s}\setminus\mathrm{dom}(\omega)}\sqcup(x\circ\omega\bigl{\lvert}_{E_{s}}))$.

Recursive and non-recursive wirings can be seen as unary and binary operators
respectively, over the set of all modules. For any $\omega$, we can define the
operators $\rightarrowtail_{\omega}$ and $\circlearrowright_{\omega}$. For
simplicity we define that $M\rightarrowtail_{\omega}M^{\prime}=\varnothing$
and $\circlearrowright_{\omega}M=\varnothing$ if the wiring $\omega$ is not
defined over the same sets as $M$ or $M^{\prime}$. Notice that both the
recursive and non-recursive wirings defined by $\omega=\varnothing$ are well
defined wiring. They define two operators, $\circlearrowright_{\varnothing}$
and $\rightarrowtail_{\varnothing}$, that will be useful later on.

###### Property 1

The following statements hold.

  1. (i)

$\forall M,\quad\circlearrowright_{\varnothing}M=M$.

  2. (ii)

$\forall M,M^{\prime},\quad
M\rightarrowtail_{\varnothing}M^{\prime}=M^{\prime}\rightarrowtail_{\varnothing}M$.

  3. (iii)

$\forall M,M^{\prime},M^{\prime\prime},\quad
M\rightarrowtail_{\varnothing}(M^{\prime}\rightarrowtail_{\varnothing}M^{\prime\prime})=(M\rightarrowtail_{\varnothing}M^{\prime})\rightarrowtail_{\varnothing}M^{\prime\prime}$.

For simplicity of notations, we will denote the empty non-recursive wiring as
the union operator over modules: $M\cup
M^{\prime}=M\rightarrowtail_{\varnothing}M^{\prime}$.

It is quite natural to want to put two modules together, by linking the input
of the first to states of the second, and conversely. Our formalism allows
this operation in two steps : first, use a non-recursive wiring to connect all
of the desired inputs of the first module to states of the second module.
Then, use a recursive wiring to connect back all of the desired inputs of the
second module to states of the first module.

We now express that recursive and non-recursive wirings are expressive enough
to construct any BAN or module, in Theorem 5.1. Our aim is to show that for
any division of a module into smaller parts (partitioning), there is a way to
get back to the initial module using only recursive and non-recursive wirings.

###### Definition 14

Let $(S,E,\alpha)$. Let $P$ be a set such that $\\{S_{p}\mid p\in P\\}$ is a
partition of $S$. We define the _corresponding partition_ of $E$ as
$\\{E_{p}=\bigcup_{s\in S_{p}}\alpha(s)\mid p\in P\\}$.

###### Definition 15

We can now develop the corresponding partition of the input declaration, and
define the partition of $M$ itself. For every $p\in P$, we define
$\alpha_{p}=\alpha\bigl{\lvert}_{S_{p}}$ over $S_{p}$ and $E_{p}$.

###### Definition 16

For every $p\in P$, let $Q_{p}$ verify $Q_{p}\cap S=\varnothing$ and
$|Q_{p}|=|S|$, and let $\tau_{p}:S\to Q_{p}$ be a bijection. For any $p\in P$,
the _sub-module_ $M_{p}$ over $(S_{p},E_{p}\cup\tau_{p}(S\setminus
S_{p}),\alpha_{p})$ is defined for $s\in S_{p}$ as, for all $x:S\to\mathbb{B}$
and for all $i:E\to\mathbb{B}$,

$M_{p}(s)(x\bigl{\lvert}_{S_{p}}\sqcup i_{p})=M(s)(x\sqcup i)\text{,}$

where $i_{p}(e)=i(e)$ if $e\in E_{p}$ and $i_{p}(e)=x(\tau^{-1}_{p}(e))$ if
$e\in\tau_{p}(S\setminus S_{p})$.

In the previous definition, the purpose of each $Q_{p}$ is to work as a
representation of the set $S$ for every sub-module $M_{p}$. Without it, every
module $M_{p}$ would have used the set $(S\setminus S_{p})\cup E_{p}$ as input
set. However our definition of wiring requires the input sets of the wired
modules to be disjoint from each other. The sets $Q_{p}$ are a workaround to
bypass this technical point.

abcdabcd$S$$S_{r}$$S_{s}$$S_{t}$ Figure 2: Interaction graphs related to
Example 2. The interaction graph of the original module is on the left and the
interaction graphs of the partition of $M$ are on the right. Notice that we
did not represent the input sets $E$, $Q_{r}$, $Q_{s}$ and $Q_{t}$.

###### Example 2

Let $S=\\{a,b,c,d\\}$, $E=\\{e\\}$, $P=\\{r,s,t\\}$ and $S_{r}=\\{a,d\\}$,
$S_{s}=\\{b\\}$ and $S_{t}=\\{c\\}$. For each $p\in P$, we define
$Q_{p}=\\{a_{p},b_{p},c_{p},d_{p}\\}$. In the module $M_{r}$,
$\alpha_{r}(a)=\varnothing$ and $\alpha_{r}(d)=\\{b_{r},c_{r}\\}$. In the
module $M_{s}$, $\alpha_{s}(b)=\\{a_{s}\\}$. In the module $M_{t}$,
$\alpha_{t}(c)=\\{e\\}$. The modules $M_{r},M_{s}$ and $M_{t}$ are defined
over disjoint sets and can be wired (see Figure 2 for an illustration).

As a reminder, the union operator over modules is defined to be the result of
an empty non-recursive wiring.

###### Theorem 5.1

Let $M$ be a module and $\\{M_{p}\mid p\in P\\}$ any partition of that module,
then there exists a recursive wiring $\omega$ such that $M=\
\circlearrowright_{\omega}\left(\bigcup_{p\in P}M_{p}\right)$.

###### Proof

We construct $\omega$ to wire every link lost in partition $P$.

Theorem 5.1 allows to say that our definition of wiring is complete: any BAN
or module can be assembled with wirings. It can be reworked more
algebraically. Let $\mathcal{M}$ denote the set of all modules (which includes
$\varnothing$), and for any $n\in\mathbb{N}$, let $\mathcal{M}_{n}$ denote the
set of all modules of size $n$ (we have
$\mathcal{M}=\bigcup_{n\in\mathbb{N}}\mathcal{M}_{n}$). For any subset
$A\subseteq\mathcal{M}$ we denote $\overline{A}^{\omega}$ the closure of $A$
by the set of wiring operators
$\bigcup_{\omega}\\{\rightarrowtail_{\omega},\circlearrowright_{\omega}\\}$.
The following result is a direct corollary of Theorem 5.1.

###### Corollary 1

The set of all modules is equal to the closure by any wiring of the set of
modules of size $1$,

$\mathcal{M}=\overline{\mathcal{M}_{1}}^{\omega}.$

Every module in $\mathcal{M}_{1}$ is of size $1$, but as the set of inputs $E$
of a module is not bounded, the set $\mathcal{M}_{1}$ is infinite. In our
opinion, this corollary is enough to demonstrate that our definition of
modules and wirings is sound.

##  6 Simulation

BANs are by nature complex systems and sometimes, we like to understand the
computational power of a subset of them by demonstrating that they are able to
simulate (or be simulated by) another subset of BANs. By _simulation_ , we
generally mean that a BAN is able to reproduce, according to some encoding,
all the possible computations of another BAN.

Simulation is a powerful way to understand the limitations and possibilities
of BANs. It is still difficult to prove if any two BANs simulate each other.
In the present paper our aim is to prove that the property of simulating any
BAN can be reduced in some cases to the property of locally simulating any
Boolean function. Locally simulating a function means that a module reproduces
any computation of that function, when the parameters of the function are
encoded in the module inputs. Our claim is that if we can locally simulate
every function of a BAN, in a way such that the simulating modules are able to
communicate with each other, then we can simulate the same BAN with a bigger
module which is obtained by a wiring over the locally simulating modules. In
this context, modules become a strong tool to reduce the complexity of
simulation (which is a global phenomena) to a local scale, which is more
tractable.

Let us go into further details. For $F$ a BAN over the set $S$, our aim is to
simulate $F$. For this purpose, for each $a\in S$, we create $M_{a}$, a module
which is defined over some sets $(T_{a},E_{a},\alpha_{a})$ and locally
simulates the function $f_{a}$. To assert this local simulation we need to
define a Boolean encoding $\phi_{a}$ over the configurations of $M_{a}$. We
also need to define how these modules communicate with each other, and in the
end how they will be wired together. For any couple $a,b\in S$ such that
$a\neq b$, we define the set $U_{a,b}$ as a subset of $T_{a}$. This set
represents all the automata of $M_{a}$ that are planned to be connected to
inputs of $M_{b}$. We can say that the elements of $U_{a,b}$ are the only way
for the module $M_{a}$ to send information to the module $M_{b}$. We define
which information is sent from $M_{a}$ to $M_{b}$ at any time with a Boolean
encoding $\phi_{a,b}$ over the set of configurations on $U_{a,b}$. By
definition we always have that if $U_{a,b}\neq\varnothing$, then
$\phi_{a}(x\bigl{\lvert}_{T_{a}})\neq\bullet\Rightarrow\phi_{a,b}(x\bigl{\lvert}_{U_{a,b}})=\phi_{a}(x\bigl{\lvert}_{T_{a}})$.
This means that if a module encodes an information ($\bullet$ being the
absence of information, i.e. in this case $\phi_{a}(x\bigl{\lvert}_{T_{a}})$
equals $0$ or $1$), the same information is sent from that module to each
module that is meant to receive information from it. In other words, all
encodings are coherent.

Now that our modules are set to communicate with each other, we only need to
wire them to each other. The precise nature of this wiring is defined, for
every pair $a,b\in S$ such that $a\neq b$, by the function $I_{a,b}:E_{b}\to
U_{a,b}$ which we call interface between $a$ and $b$. By definition:

  * •

for every $s\in U_{a,b}$, there exists $e\in E_{b}$ such that $I_{a,b}(e)=s$
(surjectivity);

  * •

for every $b\in S$, $\bigsqcup_{a}I_{a,b}$ is a total map from $E_{b}$ to
$\bigcup_{a}U_{a,b}$.

With such an interface defined for every pair $(a,b)$, the final wiring
connecting all modules together is decomposed in two steps. The first one
empty-wires every module together, the second one applies a recursive wiring
which is defined as the union of every interface $I_{a,b}$. The last condition
that we have stated over the definition of an interface lets us know that the
obtained module has no remaining inputs; it can be considered as a BAN,
defined over $T=\bigcup_{a\in S}T_{a}$. All these sets are illustrated in
Figure 3.

abcdefghijklmn$S$$T_{a}$$U_{a,b}$$T_{b}$$U_{b,c}$$T_{c}$$U_{c,d}$$T_{d}$$U_{d,a},U_{d,b}$$T$
Figure 3: Interaction graphs of the modules detailed in Example 3. The
interaction graph of the original BAN is on the left and the interaction graph
of the simulating BAN is on the right. The simulating BAN is decomposed into
four sub-modules, one for each node in $S$. Notice that we did not represent
the input sets $E_{a}$, $E_{b}$, $E_{c}$ and $E_{d}$. The connections between
the sets $T_{a}$, $T_{b}$, $T_{c}$ and $T_{d}$ are based upon the interfaces
defined in the example.

###### Example 3

Let $S=\\{a,b,c,d\\}$. Let $T_{a}=\\{e,f,g,h\\}$, $T_{b}=\\{i,j,k\\}$,
$T_{c}=\\{l,m\\}$ and $T_{d}=\\{n\\}$. Let $T=T_{a}\cup T_{b}\cup T_{c}\cup
T_{d}$. Let $E_{a}=\\{e_{g},e_{h}\\}$,
$E_{b}=\\{e_{i},e_{k},e^{\prime}_{k}\\}$, $E_{c}=\\{e_{m}\\}$ and
$E_{d}=\\{e_{n}\\}$. Let $U_{a,b}=\\{f,g\\}$, $U_{b,c}=\\{j\\}$,
$U_{c,d}=\\{l\\}$, $U_{d,a}=U_{d,b}=\\{n\\}$, and any other $U$ set empty. We
will define interfaces as the following: $I_{a,b}(e_{i})=f$,
$I_{a,b}(e_{k})=g$, $I_{b,c}(e_{m})=j$, $I_{c,d}(e_{n})=l$,
$I_{d,a}(e_{h})=n$, $I_{d,a}(e_{g})=n$ and $I_{d,b}(e^{\prime}_{k})=n$ (see
Figure 3).

###### Definition 17

Let $A$ be a set. A _Boolean encoding_ over A is a function
$\phi:(A\to\mathbb{B})\to(\\{0,1,\bullet\\})$, such that there exists at least
one $x$ such that $\phi(x)=0$ and one $x$ such that $\phi(x)=1$.

For $x:A\to\mathbb{B}$ (a Boolean configuration over a set $A$), $\phi(x)=1$
means that $x$ encodes a $1$, $\phi(x)=0$ means that $x$ encodes a $0$, and
$\phi(x)=\bullet$ means that $x$ does not encode any value. Each $\phi_{a}$ is
defined as an encoding over $T_{a}$, and each $\phi_{a,b}$ as an encoding over
$U_{a,b}$.

By definition we enforce that

$\text{if }U_{a,b}\neq\varnothing\text{, then
}\phi_{a}(x\bigl{\lvert}_{T_{a}})\neq\bullet\Rightarrow\phi_{a,b}(x\bigl{\lvert}_{U_{a,b}})=\phi_{a}(x\bigl{\lvert}_{T_{a}}).$

Given a BAN on $S$ and some $a\in S$, let us now define the local simulation
of function $f_{a}$ by a module $M_{a}$. We want to express that given any
configuration $x:S\to\mathbb{B}$, all the configurations
$x^{\prime}:T_{a}\to\mathbb{B}$ and input configurations
$i^{\prime}:E_{a}\to\mathbb{B}$ such that $x^{\prime},i^{\prime}$ encode the
same information as $x$, the result of the dynamics on $x^{\prime},i^{\prime}$
in the simulating module must encode the result of the dynamics on $x$ in the
simulated automaton. To express that $x^{\prime}$ encodes the state of $a$ in
$x$ is easy: $\phi_{a}(x^{\prime})=x_{a}$. To express that $i^{\prime}$
encodes the state of all $b\neq a$ in $x$ requires an additional notation. On
the one hand we have
$\phi_{b,a}:(U_{b,a}\to\mathbb{B})\to(\\{0,1,\bullet\\})$, and on the other
hand we have $i^{\prime}:E_{a}\to\mathbb{B}$ describing the input-
configuration of module $M_{a}$, and $I_{b,a}:E_{a}\to U_{b,a}$ describing the
interface from $b$ to $a$. To plug these objects together, we put forward the
hypothesis that if $I_{b,a}(e)=I_{b,a}(e^{\prime})$, then
$i^{\prime}(e)=i^{\prime}(e^{\prime})$ for any $e,e^{\prime}\in E_{a}$. This
hypothesis is justified by the fact that the wiring applied by $I_{b,a}$
enforces the value of two inputs connected to the same element to be the same.
Now, we define $i^{\prime}\circ I_{b,a}^{-1}$ the configuration over $U_{b,a}$
such that $i^{\prime}\circ I_{b,a}^{-1}(s)=i^{\prime}(e)$ for any $e$ such
that $I_{b,a}(e)=s$. By our hypothesis this configuration is well defined.

###### Definition 18

Let $a\in S$, $f_{a}$ be a Boolean function over $S$ and $M_{a}$ a module over
$(T_{a},E_{a},\alpha_{a})$, with $\phi_{a}$ (resp. $\phi_{b,a}$) a Boolean
encoding over $T_{a}$ (resp. $U_{b,a}$). Given a finite update mode $\Delta$
over $T_{a}$, $M_{a}$ _locally simulates_ $f_{a}$, denoted by
$M_{a}\prec_{\Delta}f_{a}$, if for all $x:S\to\mathbb{B}$,

  1. 1.

and for all $x^{\prime}:T_{a}\to\mathbb{B}$ such that
$\phi_{a}(x^{\prime})=x_{a}$,

  2. 2.

and for all $i^{\prime}:E_{a}\to\mathbb{B}$ such that for all $b\neq a$ we
have $\phi_{b,a}(i^{\prime}\circ I_{b,a}^{-1})=x_{b}$,

  3. 3.

we have:

$\phi_{a}({M_{a}}_{\Delta}(x^{\prime}\sqcup i^{\prime}))=f_{a}(x)\text{.}$

This local simulation can be defined on a wide range of update modes $\Delta$.
To ensure that the simulation works as planned at the global scale, we
restrict the range of update modes $\Delta$ used for the local simulations, to
those where no automata with input(s) are updated later than the first update.

###### Definition 19

An update mode $\Delta$ over a module $M$ is defined to be _input-first_ if
for all $k>1$ and all $s\in\Delta_{k}$, we have $\alpha(s)=\varnothing$.

###### Definition 20

We define that $M$ is able to _input-first simulate_ $f$ if there exists an
input-first $\Delta$ such that $M\prec_{\Delta}f$.

Intuitively, such update modes let us make parallel the computation of
modules; all information between modules is communicated simultaneously at the
first frame of computation (update), followed by isolated updates in each
module. To define global simulation, we introduce the global encoding
$\Phi:(S\to\mathbb{B})\to(S^{\prime}\to\mathbb{B})\cup\\{\bullet\\}$ which
always verifies that for all $x^{\prime}:S^{\prime}\to\mathbb{B}$, there
exists $x:S\to\mathbb{B}$ such that $\Phi(x)=x^{\prime}$.

###### Definition 21

Let $F$ and $F^{\prime}$ be two Boolean automata networks over $S$ and
$S^{\prime}$ respectively. We define that $F$ _simulates_ $F^{\prime}$,
denoted by $F\prec F^{\prime}$, if there exists a global encoding $\Phi$ such
that for all $x^{\prime}$, $x$ such that $\Phi(x)=x^{\prime}$, and for all
$\delta^{\prime}\subseteq S^{\prime}$, there exists a finite update mode
$\Delta$ over $S$ such that
$\Phi(F_{\Delta}(x))=F^{\prime}_{\delta^{\prime}}(x^{\prime})$.

Given the definitions of local and global simulation, for any BAN $F$ over a
set $S$, we define each module $M_{a}$ as earlier, each defined over
$(T_{a},E_{a},\alpha_{a})$, along side each set $U_{a,b},I_{a,b}$ and each
encoding $\phi_{a},\phi_{a,b}$.

###### Theorem 6.1

Let $F$ be a BAN over $S$. For each $a\in S$, let $M_{a}$ be a module over
$(T_{a},E_{a},\alpha_{a})$ that locally simulates $F(a)$ in an input-first
way. There exists a recursive wiring $\omega$ over $T=\bigcup_{a\in S}T_{a}$
such that

$\circlearrowright_{\omega}\left(\bigcup_{a\in S}M_{a}\right)\prec F\text{.}$

###### Proof

We prove that the execution of the module $M$ obtained from the wiring
$\omega$ can be built from the execution of each $M_{a}$. We apply the
hypothesis of local simulation on each $M_{a}$, and obtain a global
simulation.

This theorem helps us investigate if every BAN can be simulated by a BAN with
a given property, hence justifying that theoretical studies can impose some
restrictions without loss of generality. If every function $f$ can be locally
simulated by a given module with a property $\mathcal{P}$, and if property
$\mathcal{P}$ is preserved over wirings, then we know that any BAN can be
simulated by another BAN with the property $\mathcal{P}$. This is formally
proven for the following cases.

###### Corollary 2

Let $F$ be a BAN. There exists $F^{\prime}$ such that $F^{\prime}\prec F$ and
every function of $F^{\prime}$ is a disjunctive clause.

###### Corollary 3

Let $F$ be a BAN. There exists $F^{\prime}$ such that $F^{\prime}\prec F$ and
every function of $F^{\prime}$ is monotone.

###### Proof

Both of theses results are obtained by replacing the automata of $F$ by
modules that locally simulates them. For disjunctivity, the module has one
automaton for each clause of the conjunctive normal form of the simulated
function, and one for the result (using De Morgan’s law we convert the outer
conjunction to a disjunction). For monotony, we use a lemma that shows that we
can always construct a monotone function from any function at the cost of
duplicating each variable. Using this lemma we construct a network with twice
the automata which locally simulates any function. The results are obtained by
the Theorem 6.1.

It can seem strange that this particular theorem applies to BANs and not to
modules (as it would be a more general result). Such a result would need a
definition of simulation between modules, and such a definition would imply an
interpretation of the information provided by the simulating module’s inputs.
We choose not to develop this particular idea, as this theorem was only meant
to apply to BANs, but a generalisation of this result to modules would be a
good subject for future works.

##  7 Examples

To illustrate and justify the notions that are presented in Section 2, we
shall now present two examples of BANs that can be partially understood by
cutting them into modules. The first example is a toy BAN illustrated in
Figure 4. In this representation we assume the function of each automaton to
be a disjunctive clause with one literal for each incident edge, the sign of
which dictates the sign of the literal.

abcdefgh++$+$$-$$-$$-$$-$$+$$-$$+$$\
-$$-$$+$abcdefgh++$-$$-$$-$$-$$-$$+$$+$$-$$+$$-$$+$$F$$M_{1}$$M_{2}$$M_{3}$
Figure 4: Representation of a handmade Boolean automata network $F$ next to
the three different modules $M_{1}$, $M_{2}$ and $M_{3}$ that compose it. The
function of each automaton is defined as a disjunctive clause with a positive
literal for each incident “$+$” edge, and a negative literal for each incident
“$-$” edge. For example, $f_{h}(x)=x_{c}\vee\neg x_{e}$.

Looking at this example, it does not seem easy to express the entire behaviour
of the BAN $F$. Its representation is a strongly connected graph with multiple
interconnected positive and negative cycles. Yet, cutting this graph into
multiple modules and analysing the functionality of each of them is an easy
way to understand interesting parts of the dynamics of the network.

By assuming the decomposition of $F$ as shown in Figure 4, we can start to
attach a functionality to each module. Module $M_{1}$ is a positive cycle,
where the configuration $x_{a}=x_{d}=1$ is a fixed point (whatever the input).
Its functionality can be identified as a “one time button” that cannot be
pushed back. Module $M_{2}$ is a negative cycle, which are known for their
long limit cycles. The difference here is that as $M_{2}$ has two inputs, its
behaviour can be stabilised into a fixed point by a fixed input. For example,
the fixed point $x_{b}=x_{e}=1,x_{c}=0$ can be obtained with the constant
input $i_{b}=1,i_{e}=0$. Finally, the module $M_{3}$ is acyclic and thus only
computes the Boolean function $\neg i_{g}\vee(\neg i_{h}\wedge
i_{h^{\prime}})$. It follows that $M_{3}$ stabilises to a fixed point under
any constant input.

This simple analysis leads us to the following conclusion : every fair
execution (meaning executing every automaton an infinite amount of time) of
$F$ which verifies $x_{a}=x_{d}=1$ at any moment stabilises into a fixed
point. This is true because $x_{a}=x_{d}=1$ implies that the “one time button”
of $M_{1}$ is pushed in, which locks the behaviour of $M_{2}$ into a fixed
point, which leads $M_{3}$ to compute a Boolean function over a fixed input.
This somewhat informal demonstration has led us to a conclusion that was not
easily implied by the architecture of the network, showcasing the usefulness
of understanding networks as composition of parts to which one can assign
functionalities.

The second example is drawn from a model predicting the cell cycle sequence of
fission yeast [6]. This network is represented in Figure 5, and can be
decomposed into a more abstract network, where each node represents a module
of the original network. This network is represented in Figure 6 and its
modules are constructed as follows:
$C=\\{Rum1,Ste9\\},D=\\{Cdc,Cdc*\\},F=\\{Cdc25\\},G=\\{Mik\\},I=\\{Start,SK\\},J=\\{PP,Slp1\\}$.
A quick analysis of these modules leads us to sort them into three categories
: cycles ($C,D$), functions ($F,G$) and igniters ($I,J$). Let us now explain
this organisation in an informal way.

The two cycle modules $C$ and $D$ are organised in a 4-cycle of negative
feedback which means that if considered separately from the rest of the
network, those two modules would behave as antagonists: in most cases, when
the automata of $C$ (resp. $D$) are evaluated to $1$, the automata of $D$
(resp. $C$) will be evaluated to $0$. Modules $F$ and $G$ can be viewed as
functions which help $D$ and $C$ respectively to be evaluated to $1$; they
both are influenced by $J$ in different ways. Modules $I$ and $J$ are called
igniters because they turn themselves to $0$ every time they are evaluated to
$1$, but not before influencing the other nodes. Module $I$ inhibits $C$ when
activated, and can be considered as the input of the whole network. Module $J$
is activated by $D$, activates $C$ and $G$, and inhibits $F$.

From this we can conclude that if the network stabilises, it will more likely
stabilise by evaluating $C$ to $1$ and $D$ to $0$. This conclusion arises from
the fact that $D$ activates $J$, which in turn inhibits $D$ directly, but also
inhibits $F$ (which activates $D$) and activates $G$ (which inhibits $D$).
This also means that $F$ will be evaluated to $0$ and $G$ to $1$. Finally, $I$
and $J$ will naturally be evaluated to $0$ because of the natural negative
feedback that compose them. This particular evaluation of the network (only
$C$ and $G$ to $1$) is actually the main fixed point of the network’s dynamics
put forward in [6] and is named $G1$. This shows that such a fixed point can
be described without the need to compute the $2^{10}=1024$ different
configurations of the network and their dynamics.

StartSKCdcRum1Ste9PPSlp1Cdc25MikCdc* Figure 5: Representation of the network
simulating the cell cycle sequence of fission yeast extracted from [6].
Activating interactions are represented by simple arrows and inhibiting
interactions by flat arrows. The detail of each node’s function is available
in the original paper. CDGIJF Figure 6: Abstract representation of the
interactions between the modules $C,D,F,G,I$ and $J$ based upon the network
represented in Figure 5.

##  8 Conclusion

The two theorems formulated in this article tell us that seeing BANs as
modular entities is a way to discover useful results. With the simple addition
of inputs to BANs, we have expressed a general simulation structure that can
be used to understand the computational nature and limits of given properties
over BANs. Let us underline that all the definitions and results can be
applied to BANs and modules defined over countably infinite sets of automata
and inputs.

Wherever Turing-completeness is observed, complex behaviours emerge that
cannot be simply or quickly formulated from the basic rules of the
computation. In such situations, the solution is either to compute every
single possibility to capture the whole dynamics of the observed system, or to
simplify the model. We believe that the framework developed in this paper is a
strong candidate to enable us to decompose complex networks into parts with
tractable functionalities, and to make conclusions about the whole network at
a cheaper cost. This approach is still very informal at this moment and will
be the focus of further developments.

#### Acknowledgements

This work has been supported “Investissement d’avenir” program
ANR-16-CONV-00001 and PACA Project Fri 2015_01134.

## References

  * [1] A. Alcolei, K. Perrot, and S. Sené.  On the flora of asynchronous locally non-monotonic Boolean automata networks.  In Proc. of SASB’15, volume 326 of ENTCS, pages 3–25, 2016\.
  * [2] U. Alon.  Biological networks: the tinkerer as an engineer.  Science, 301:1866–1867, 2003.
  * [3] J. Aracena, Luis Gómez, and L. Salinas.  Limit cycles and update digraphs in Boolean networks.  Discrete Appl. Math., 161:1–12, 2013.
  * [4] G. Bernot and F. Tahi.  Behaviour preservation of a biological regulatory network when embedded into a larger network.  Fund. Inform., 91:463–485, 2009.
  * [5] M. Cook.  Universality in elementary cellular automata.  Complex Systems, 15:1–40, 2004.
  * [6] Bornholdt S Davidich M.I.  Boolean network model predicts cell cycle sequence of fission yeast.  PLoS One, 3:e1672, 2008.
  * [7] F. Delaplace, H. Klaudel, T. Melliti, and S. Sené.  Analysis of modular organisation of interaction networks based on asymptotic dynamics.  In Proc. of CMSB’12, volume 7605 of LNCS, pages 148–165, 2012\.
  * [8] J. Demongeot, E. Goles, M. Morvan, M. Noual, and S. Sené.  Attraction basins as gauges of robustness against boundary conditions in biological complex systems.  PLoS One, 5:e11793, 2010.
  * [9] T. Feder.  Stable networks and product graphs.  PhD thesis, Stanford University, 1990.
  * [10] F. Fogelman, E. Goles, and G. Weisbuch.  Transient length in sequential iteration of threshold functions.  Discrete Appl. Math., 6:95–98, 1983.
  * [11] E. Goles and L. Salinas.  Comparison between parallel and serial dynamics of Boolean networks.  Theor. Comput. Sci., 396:247–253, 2008.
  * [12] S. A. Kauffman.  Metabolic stability and epigenesis in randomly constructed genetic nets.  Journal of Theoretical Biology, 22:437–467, 1969.
  * [13] R. Milo, S. Shen-Orr, S. Itzkovitz, N. Kashtan, D. Chklovskii, and U. Alon.  Network motifs: simple building blocks of complex networks.  Science, 298:824–827, 2002.
  * [14] M. Noual.  Updating Automata Networks.  PhD thesis, École Normale Supérieure de Lyon, 2012.
  * [15] F. Robert.  Discrete iterations: a metric study.  Springer, 1986.
  * [16] H. Siebert.  Dynamical and structural modularity of discrete regulatory networks.  In Proc. of COMPMOD’09, volume 6 of EPTCS, pages 109–124, 2009.
  * [17] R. Thomas.  Boolean formalization of genetic control circuits.  J. Theor. Biol., 42:563–585, 1973.

##  Appendix 0.A Proofs

###### Property 1

The following statements hold.

  1. (i)

$\forall M,\quad\circlearrowright_{\varnothing}M=M$.

  2. (ii)

$\forall M,M^{\prime},\quad
M\rightarrowtail_{\varnothing}M^{\prime}=M^{\prime}\rightarrowtail_{\varnothing}M$.

  3. (iii)

$\forall M,M^{\prime},M^{\prime\prime},\quad
M\rightarrowtail_{\varnothing}(M^{\prime}\rightarrowtail_{\varnothing}M^{\prime\prime})=(M\rightarrowtail_{\varnothing}M^{\prime})\rightarrowtail_{\varnothing}M^{\prime\prime}$.

###### Proof

$\forall
M,M^{\prime},M\rightarrowtail_{\varnothing}M^{\prime}=M^{\prime}\rightarrowtail_{\varnothing}M\text{.}$

By definition, $M\rightarrowtail_{\varnothing}M^{\prime}$ and
$M^{\prime}\rightarrowtail_{\varnothing}M$ are both defined on $(S\cup
S^{\prime},E\cup E^{\prime},\alpha\sqcup\alpha^{\prime})$. For any $s\in S$,
$M\rightarrowtail_{\varnothing}M^{\prime}(s)=M^{\prime}\rightarrowtail_{\varnothing}M(s)$
and for $s^{\prime}\in S^{\prime}$,
$M\rightarrowtail_{\varnothing}M^{\prime}(s^{\prime})=M^{\prime}\rightarrowtail_{\varnothing}M(s^{\prime})$.

$\forall M,\circlearrowright_{\varnothing}M=M\text{.}$

By a similar argument, $\circlearrowright_{\varnothing}M$ is by definition
defined on $(S,E,\alpha)$ such that $\circlearrowright_{\varnothing}M(s)=M(s)$
for any $s\in S$.

$\forall
M,M^{\prime},M",M\rightarrowtail_{\varnothing}(M^{\prime}\rightarrowtail_{\varnothing}M")=(M\rightarrowtail_{\varnothing}M^{\prime})\rightarrowtail_{\varnothing}M"\text{.}$

By definition, the left side of this equation is defined over $(S\cup
S^{\prime}\cup S",E\cup E^{\prime}\cup
E",\alpha\sqcup\alpha^{\prime}\sqcup\alpha")$ as is the right side of this
equation. The two modules defining the same functions, we obtain the result.∎

###### Theorem 0.A.1

Let $M$ be a module and $\\{M_{p}\mid p\in P\\}$ a partition of that module.
There exists a recursive wiring $\omega$ such that

$M=\ \circlearrowright_{\omega}\left(\bigcup_{p\in P}M_{p}\right)\text{.}$ (1)

###### Proof

By definition of the empty wiring, the module $\bigcup_{p\in P}M_{p}$ is
defined over $(S,E\cup\bigcup_{p\in P}\tau_{p}(S\setminus
S_{p}),\bigsqcup_{p\in P}\alpha_{p})$ and for all $s\in S$,
$x:S\rightarrow\mathbb{B}$ and $i:E\rightarrow\mathbb{B}$ verifies

$\left(\bigcup_{p\in P}M_{p}\right)(s)(x\sqcup i^{\prime})=M(s)(x\sqcup
i)\text{.}$ (2)

Knowing that $i^{\prime}(e)=i(e)$ for $e\in E_{s}$, and
$i^{\prime}(s)=x(\tau^{-1}_{p}(s))$ for $s\in Q_{p}$. Let $\omega$ be the
recursive wiring over $\bigcup_{p\in P}M_{p}$ with domain $\bigcup_{p\in
P}\tau_{p}(S\setminus S_{p})$ such that $\omega(q)=\tau_{p}^{-1}(q)$ given p
such that $q\in Q_{p}$.

By definition of the recursive wiring, the module
$\circlearrowright_{\omega}(\bigcup_{p\in P}M_{p})$ is defined over the set
$(S,E,\alpha)$. For all $s,x,i$, we now have that

$\circlearrowright_{\omega}\left(\bigcup_{p\in P}M_{p}\right)(s)(x\sqcup
i)=\left(\bigcup_{p\in P}M_{p}\right)(s)(x\sqcup
i\bigl{\lvert}_{E_{s}}\sqcup(x\circ\omega\bigl{\lvert}_{\tau_{p}(S\setminus
S_{p})}))\text{.}$ (3)

By our definitions of $\omega$ and $i^{\prime}$, we have that
$i^{\prime}=i\bigl{\lvert}_{E_{s}}\sqcup(x\circ\omega\bigl{\lvert}_{\tau_{p}(S\setminus
S_{p})})$. From that, and Equations 2 and 3, we infer that for all $s,x,i$:

$\circlearrowright_{\omega}\left(\bigcup_{p\in P}M_{p}\right)(s)(x\sqcup
i)=M(s)(x\sqcup i)\text{.}$

Therefore for any $s$:

$\circlearrowright_{\omega}\left(\bigcup_{p\in P}M_{p}\right)(s)=M(s)\text{,}$

which concludes the proof. ∎

###### Corollary 1

The set of all modules is equal to the closure by any wiring of the set of
modules of size $1$ :

$\mathcal{M}=\overline{\mathcal{M}}_{1}^{\omega}\text{.}$

###### Proof

Trivially, $\overline{\mathcal{M}}_{1}^{\omega}\subseteq\mathcal{M}$. For any
$M\in\mathcal{M}$ of size $n$, we know by Theorem 0.A.1 that in particular the
$n$-partition of $M$ into sub-modules of size $1$ can be wired into the
original module $M$. Therefore
$\mathcal{M}=\overline{\mathcal{M}}_{1}^{\omega}$.∎

###### Theorem 0.A.2

Let $F$ be a BAN over $S$. Let $\\{M_{a}\mid a\in S\\}$ be a set such that for
every $a$, $M_{a}$ is a module over $(T_{a},E_{a},\alpha_{a})$ that simulates
$F(a)$ in a input-first way. There exists $\omega$ a recursive wiring over $T$
such that :

$\circlearrowright_{\omega}\left(\bigcup_{a\in S}M_{a}\right)\prec F\text{.}$

###### Proof

By definition of the empty wiring, $\bigcup_{a\in S}M_{a}$ is defined over
$(T,\bigcup_{a\in S}E_{a},$ $\bigsqcup_{a\in S}\alpha_{a})$. Let
$\omega=\bigcup_{a,b\in S,a\neq b}I_{a,b}$. By definition of $I_{a,b}$, we can
easily see that the module $M=\ \circlearrowright_{\omega}\left(\bigcup_{a\in
S}M_{a}\right)$ is defined over $(T,\varnothing,s\mapsto\varnothing)$ and can
be seen as a Boolean automata network. Let us prove that, for all $a\in S$,
for all input-first simulating update mode $\Delta$ for the module $M_{a}$,
for any $\Delta^{\prime}$ update mode over $T\setminus T_{a}$, and for any
$x:T\rightarrow\mathbb{B}$, the following equation holds:

$M_{\Delta\cup\Delta^{\prime}}(x)\bigl{\lvert}_{T_{a}}={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\text{.}$
(4)

At the first step of the execution, the wiring $\omega$ implies that for any
$s\in T_{a}$, for any $x$, $M(s)(x)$ $=$ $\left(\bigcup_{a\in
S}M_{a}\right)(s)(x\sqcup(x\circ\omega))$. From the definition of the empty
wiring, we can deduce in particular that $M(s)(x)$ $=$ $M_{a}(s)($
$x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\omega\bigl{\lvert}_{E_{a}}))$. By
definition of the interfaces, this notation is equivalent to $\forall s\in
T_{a},M(s)(x)=M_{a}(s)(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))$.

Let us define $A=\\{s\in T_{a}\mid\alpha(s)\neq\varnothing\\}$ and
$B=T_{a}\setminus A$. By the definition of $\Delta$, we know that
$s\in\Delta_{k}$ with $k>0$ implies $s\in B$.
Let us look at the $A$ part of this problem. Let $\delta=\Delta_{0}$ and
$\delta^{\prime}=\Delta^{\prime}_{0}$. We can trivially deduce from the
previous statement that:

$M_{\delta\cup\delta^{\prime}}(x)\bigl{\lvert}_{A}={M_{a}}_{\delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\bigl{\lvert}_{A}\text{.}$

Furthermore, there is no $s\in A$ such that $s\in\Delta_{k}$ for any $k>0$. We
can simply conclude since no update is made to any function of $A$ in the rest
of the execution that
$M_{\delta\cup\delta^{\prime}}(x)\bigl{\lvert}_{A}=M_{\Delta\cup\Delta^{\prime}}(x)\bigl{\lvert}_{A}$,
and that
${M_{a}}_{\delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\bigl{\lvert}_{A}={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\bigl{\lvert}_{A}$.
In conclusion of this $A$ part,
$M_{\Delta\cup\Delta^{\prime}}(x)\bigl{\lvert}_{A}={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}$
$\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\bigl{\lvert}_{A}$.
Let us now consider the $B$ part of the problem. For $s\in B$, we have
$M(s)(x)=M_{a}(s)(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\omega\bigl{\lvert}_{E_{s}}))$.
By definition of $B$, $s\in B$ implies $E_{s}=\varnothing$. We can conclude
that $\forall s\in B,M(s)(x)=M_{a}(s)(x\bigl{\lvert}_{T_{a}})$. We deduce, for
any $\delta\subseteq T_{a}$ and $\delta^{\prime}\subseteq T\setminus T_{a}$,
that
$M_{\delta\cup\delta^{\prime}}(x)\bigl{\lvert}_{B}={M_{a}}_{\delta}(x\bigl{\lvert}_{T_{a}}\sqcup
i)\bigl{\lvert}_{B}$, for $i$ any input configuration over $E_{a}$. By a
simple recursive demonstration, we can easily show that
$M_{\Delta\cup\Delta^{\prime}}(x)\bigl{\lvert}_{B}={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup
i)\bigl{\lvert}_{B}$.
Reuniting the $A$ and $B$ parts of this demonstration, we obtain that
$M_{\Delta\cup\Delta^{\prime}}(x)$
$={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\bigl{\lvert}_{A}\cup{M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup
i)\bigl{\lvert}_{B}$. Assuming $i=x\circ\bigsqcup_{b}I_{b,a}$, we obtain
$M_{\Delta\cup\Delta^{\prime}}(x)={M_{a}}_{\Delta}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))$,
and prove the lemma described in Equation 4.

Let us now define
$\Phi:(T\rightarrow\mathbb{B})\rightarrow(S\rightarrow\mathbb{B})\cup\\{\varnothing\\}$
such that, for any $x:T\rightarrow\mathbb{B}$, $\Phi(x)=\varnothing$ if there
exists $a\in S$ such that $\phi_{a}(x\bigl{\lvert}_{T_{a}})=\varnothing$, and
$\Phi(x)(a)=\phi_{a}(x\bigl{\lvert}_{T_{a}})$ otherwise. Let $x$ and
$x^{\prime}$ such that $\Phi(x)=x^{\prime}$, and $x^{\prime}\neq\varnothing$.
Let $\delta\subseteq S$ be an update over $F$. Let us define, for any
$a\in\delta$, the update mode $\Delta_{a}$ such that $\Delta_{a}$ is an input-
first update mode upon which $M_{a}$ simulates the function $F(a)$ ; by
hypothesis such an update mode can always be found.
Let us define the update mode $\Delta$ over $T$ such that
$\Delta=\bigcup\\{\Delta_{a}\mid a\in\delta\\}$. We will now prove that
$\Phi(M_{\Delta}(x))=F_{\delta}(x^{\prime})$. First, we can clearly see that
$M_{\Delta}(x)=\bigsqcup\\{M_{\Delta}(x)\bigl{\lvert}_{T_{a}}\mid a\in S\\}$,
which can be developed into
$M_{\Delta}(x)=\bigsqcup\\{M_{\Delta}(x)\bigl{\lvert}_{T_{a}}\mid
a\in\delta\\}\sqcup\bigsqcup\\{x\bigl{\lvert}_{T_{a}}\mid a\in
S\setminus\delta\\}$, from which we infer:

$M_{\Delta}(x)=\bigsqcup\\{M_{\Delta_{a}\cup\bigcup_{b\in\delta,b\neq
a}\Delta_{b}}(x)\bigl{\lvert}_{T_{a}}\mid
a\in\delta\\}\sqcup\bigsqcup\\{x\bigl{\lvert}_{T_{a}}\mid a\in
S\setminus\delta\\}\text{.}$

Using the lemma formulated in Equation 4, this can be rewritten into:

$M_{\Delta}(x)=\bigsqcup_{a\in\delta}{M_{a}}_{\Delta_{a}}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a}))\sqcup\bigsqcup_{a\in
S\setminus\delta}x\bigl{\lvert}_{T_{a}}\text{.}$

As the result of an execution of the module $M_{a}$ is always defined as a
configuration over $T_{a}$, we can infer the following encoding of
$M_{\Delta}(x)$ by $\Phi$ :

$\Phi(M_{\Delta}(x))(a)=\begin{array}[]{\\{}{ll}.\phi_{a}({M_{a}}_{\Delta_{a}}(x\bigl{\lvert}_{T_{a}}\sqcup(x\circ\bigsqcup_{b}I_{b,a})))&\text{
if }a\in\delta\\\ \phi_{a}(x\bigl{\lvert}_{T_{a}})&\text{ if }a\in
S\setminus\delta\end{array}\text{.}$

We know by definition of $x$ and $x^{\prime}$ that
$\phi_{a}(x\bigl{\lvert}_{T_{a}})=x^{\prime}_{a}$ and that $\phi_{b,a}(x\circ
I_{b,a}\circ
I^{-1}_{b,a})=\phi_{b,a}(x\bigl{\lvert}_{U_{b,a}})=\phi_{b}(x\bigl{\lvert}_{T_{b}})=x^{\prime}_{b}$
by definition of $\phi_{b,a}$. From this we can apply the local simulation
definition and obtain:

$\Phi(M_{\Delta}(x))(a)=\begin{array}[]{\\{}{ll}.f_{a}(\Phi(x))&\text{ if
}a\in\delta\\\ \phi_{a}(x\bigl{\lvert}_{T_{a}})&\text{ if }a\in
S\setminus\delta\end{array}\\\
\iff\Phi(M_{\Delta}(x))(a)=\begin{array}[]{\\{}{ll}.f_{a}(\Phi(x))&\text{ if
}a\in\delta\\\ \Phi(x)(a)&\text{ if }a\in
S\setminus\delta.\end{array}\text{.}$

Futhermore, by the definition of an update over $F$, we can write that:

$F_{\delta}(x^{\prime})(a)=\begin{array}[]{\\{}{ll}.f_{a}(x^{\prime})&\text{
if }a\in\delta\\\ x^{\prime}(a)&\text{ if }a\in
S\setminus\delta\end{array}\text{.}$

Finally, by definition of $x^{\prime}=\Phi(x)$:

$F_{\delta}(x^{\prime})(a)=\begin{array}[]{\\{}{ll}.f_{a}(\Phi(x))&\text{ if
}a\in\delta\\\ \Phi(x)(a)&\text{ if }a\in S\setminus\delta\end{array}\text{,}$

which implies $\Phi(M_{\Delta}(x))=F_{\delta}(x^{\prime})$, and concludes the
proof.∎

###### Corollary 2

Let $F$ be a BAN. There exists $F^{\prime}$ such that $F^{\prime}\prec F$ and
every function of $F^{\prime}$ is a disjunctive clause.

###### Proof

With Theorem 6.1 in mind, we only need to demonstrate that for any function
$f$, there exists a module locally simulating it in a input-first way, in
which every function is a disjunctive clause.

Let us consider $F$ a BAN set over $S$. Let $a\in S$. We decompose $f_{a}$
into a set of disjunctive clauses $C_{a}$ such that
$f_{a}(x)=\bigwedge\limits_{c\in C_{a}}c(x)$.

Let $M_{a}=(T_{a},E_{a},\alpha_{a})$ be a module with $T_{a}=\\{u_{c}\mid c\in
C\\}\cup\\{r_{a}\\}$, $E_{a}=\\{e_{b,c,a} \mid a\neq b\text{, and the variable
} x_{b}\text{ is included in clause }c\\}$. For all $b,c$,
$e_{b,c,a}\in\alpha(u_{c})$ if and only if $x_{b}$ is included in clause $c$.
For $c\neq c^{\prime}$, $e_{b,c,a}\notin\alpha(u_{c}^{\prime})$ and
$\alpha(r_{a})=\varnothing$.

For $c\in C_{a}$, $x$ a configuration over $T_{a}$ and $e$ a configuration
over $E_{a}$, $M_{a}(u_{c})$ is the function described by
$f_{u_{c}}(x,e)=c(x_{a}\mapsto\neg x(r_{a})\sqcup x_{b}\mapsto\neg
e(e_{b,c,a}))$. The function $M(r)$ is the function
$f_{r_{a}}(x,e)=\bigvee\limits_{c\in C_{a}}\neg x(u_{c})$.

This local module is shaped as a pyramid where the base is constitued of one
node for every disjunctive clause of the simulated function, and the top of
exactly one node that represents the result of the function. It follows from
this definition that every function of this module is a disjunctive clause. An
illustrated example of such a local module is presented in Figure 7.

$r_{a}$$u_{c}$$u_{c^{\prime}}$$-$$-$$-$$+$$-$$e_{b,c^{\prime},a}$$e_{d,c^{\prime},a}$$\neg
f_{a}(x)$ Figure 7: Interaction graph of the locally disjunctive module for
the example function $f_{a}(x)=x_{a}\wedge(\neg x_{b}\vee x_{d})$. We name the
clauses of $f_{a}$ as $c=x_{a}$ and $c^{\prime}=\neg x_{b}\vee x_{d}$. Notice
that most of the signs are inversed to simulate a AND gate.

We define $U_{b,a}$ such that $U_{b,a}=\\{r_{a}\\}$ if the variable $x_{b}$ is
included in one of the clauses of the function $f_{a}$, and
$U_{b,a}=\varnothing$ otherwise.

The encodings $\phi_{a}$ and $\phi_{b,a}$ for every $b$ such that
$U_{b,a}\neq\varnothing$ are defined such that
$\phi_{a}(x)=\phi_{b,a}(x\bigl{\lvert}_{U_{b,a}})=\neg x(r_{a})$. This means
that the node $r$ represents the inverse of the result of the function.

We always define $I_{b,a}(e_{b,c,a})=r_{b}$. More intuitively, to resolve the
value of the variable $x_{b}$ in a clause of $f_{a}$, look for the value of
the node $r_{b}$ in the local module $M_{b}$. We reverse it back to the
correct value thanks to the inversion of each input of each clause automaton.

###### Lemma 1

$M_{a}$ locally simulates $f_{a}$ in a input-first way.

Let $\Delta_{a}=(\\{u_{c}\mid c\in C_{a}\\},\\{r_{a}\\})$ be an input-first
update mode for the module $M_{a}$. We will sometimes note
$\Delta_{a}=(\delta,\delta_{r})$ in further developments.

Let $x$ be a configuration over $F$. Let $x^{\prime}$ be a configuration over
$T_{a}$ such that $\phi_{a}(x^{\prime})=x_{a}$. Let $i^{\prime}$ be an input
configuration over $E_{a}$ such that for any $b\neq a$,
$\phi_{b,a}(i^{\prime}\circ I^{-1}_{b,a})=x_{b}$.

Such a $x^{\prime}$ is a configuration over $T_{a}$ with
$x^{\prime}(r_{a})=\neg x_{a}$. Such a $i^{\prime}$ is a configuration over
$E_{a}$ such that $i^{\prime}(e_{b,c,a})=\neg x_{b}$ for every $b$ and $c$.
Such configurations are well defined and can always be found.

To prove the above lemma, we have to show that
$\phi_{a}(M_{a\Delta_{a}}(x^{\prime}\sqcup i^{\prime}))=f_{a}(x)$, which can
be simplified into $\neg M_{a\Delta_{a}}(x^{\prime}\sqcup
i^{\prime})(r_{a})=f_{a}(x)$. By the definition of an execution over a module,
this can be developed into :

$M_{a\Delta_{a}}(x^{\prime}\sqcup
i^{\prime})(r_{a})=f_{r_{a}}(M_{a\delta}(x^{\prime}\sqcup
i^{\prime}),i^{\prime})\\\ =\bigvee\limits_{c\in C_{a}}\neg M_{a
\delta}(x^{\prime}\sqcup i^{\prime})(u_{c})=\bigvee\limits_{c\in C_{a}}\neg
c(x_{a}\mapsto\neg x^{\prime}(r_{a})\sqcup x_{b}\mapsto\neg
i^{\prime}(e_{b,c,a}))\\\ =\neg\bigwedge\limits_{c\in C_{a}}c(x_{a}\mapsto\neg
x^{\prime}(r_{a})\sqcup x_{b}\mapsto\neg i^{\prime}(e_{b,c,a})).$

By the above hypothesis, this can be simplified into :

$M_{a\Delta_{a}}(x^{\prime}\sqcup
i^{\prime})(r_{a})=\neg\bigwedge\limits_{c\in C_{a}}c(x_{a}\mapsto x_{a}\sqcup
x_{b}\mapsto x_{b}),$

which let us simply conclude that :

$\neg M_{a\Delta_{a}}(x^{\prime}\sqcup
i^{\prime})(r_{a})=\bigwedge\limits_{c\in C_{a}}c(x)=f_{a}(x)$

wich proves the lemma. From this result and the fact that the property that
function are locally defined by disjunctive functions isn’t broken by any
wiring, we conclude the result.∎

###### Corollary 3

Let $F$ be a BAN. There exists $F^{\prime}$ such that $F^{\prime}\prec F$ and
every function of $F^{\prime}$ is monotone.

###### Proof

To prepare this proof we must first obtain the following result.

###### Lemma 2

Let $x:S\to\mathbb{B}$. Let $f$ be a Boolean function over $S$. Let
$S^{\prime}=\\{s,s^{-}\mid s\in S\\}$. There exists $f^{\prime}$ a monotone
Boolean function over $S^{\prime}$ such that $f(x)=f^{\prime}(x\sqcup
s^{-}\mapsto\neg x(s))$.

For reminder, we assume that $x\leq x^{\prime}$ if and only if $x(s)\leq
x^{\prime}(s)$ for every $s\in S$, and that $f^{\prime}$ is monotone if and
only if $x\leq x^{\prime}\Rightarrow f^{\prime}(x)\leq
f^{\prime}(x^{\prime})$.

For $x^{\prime}$ an execution over $S^{\prime}$, and $s\in S$, we note
$code(x^{\prime},s)\Leftrightarrow x^{\prime}(s)=\neg x^{\prime}(s^{-})$. Let
$f$ be a Boolean function over $S$.

We define $f^{\prime}$ over the set $S^{\prime}$ as the following :

$f^{\prime}(x^{\prime})=\begin{array}[]{\\{}{ll}.f(x^{\prime}\bigl{\lvert}_{S})&\text{
if for every }s\in S,code(x^{\prime},s)\\\ 1&\text{ if for every }s\in S,\neg
code(x^{\prime},s)\Rightarrow x^{\prime}(s)=x^{\prime}(s^{-})=1\\\ 0&\text{
otherwise}\end{array}.$

From this definition we clearly see that for all configurations $x$ over $S$,
$f(x)=f^{\prime}(x\sqcup s^{-}\mapsto\neg x(s))$. Let us now show that
$f^{\prime}$ is monotone.

Let $x^{\prime}$ and $x"$ be two configurations over $S^{\prime}$, such that
$x^{\prime}<x"$. This implies that for all $s^{\prime}\in S^{\prime}$,
$x^{\prime}(s^{\prime})\leq x"(s^{\prime})$ and that there is at least one
$s^{\prime}\in S^{\prime}$ such that $x^{\prime}(s^{\prime})<x"(s^{\prime})$.
This clearly implies that the propositions $\forall s\in S,code(x^{\prime},s)$
and $\forall s\in S,code(x",s)$ cannot both be true.

Let us suppose $\forall s\in S,code(x^{\prime},s)$ and $\exists s\in S,\neg
code(x",s)$. As $x^{\prime}<x"$, for every $s\in S$ such that $\neg
code(x",s)$, we now that $x"(s)=x"(s^{-})=1$. This implies that
$f^{\prime}(x")=1$, and that $f^{\prime}(x^{\prime})\leq f^{\prime}(x")$.

Let us now suppose that $\exists s\in S,\neg code(x^{\prime},s)$ and $\forall
s\in S,code(x",s)$. By a similar argument, we now suppose that for every $s\in
S$ such that $\neg code(x^{\prime},s)$, we have that
$x^{\prime}(s)=x^{\prime}(s^{-})=0$. This implies that
$f^{\prime}(x^{\prime})=0$, and $f^{\prime}(x^{\prime})\leq f^{\prime}(x")$.

Let us finally suppose that $\exists s\in S,\neg code(x^{\prime},s)$ and
$\exists s\in S,\neg code(x",s)$. In this case, we know that
$f^{\prime}(x^{\prime})=1\Rightarrow f^{\prime}(x")=1$ since $x^{\prime}<x"$.
Assuming $f^{\prime}(x^{\prime})=0$ naturally implies
$f^{\prime}(x^{\prime})\leq f^{\prime}(x")$. This concludes the proof of Lemma
2.

Let $F$ be a BAN defined over set $S$. For every $a\in S$, we define
$M_{a}=(T_{a},E_{a},\alpha_{a})$ a module with $T_{a}=\\{u_{a,-},u_{a,+}\\}$,
$E_{a}=\\{e_{b,a,+},e_{b,a,-}\mid x_{b}\text{ is included in }f_{a}\\}$. The
function $\alpha$ is such that $e_{b,a,+}\in E_{a}\Rightarrow
e_{b,a,+}\in\alpha(u_{a,+})$ and $e_{b,a,-}\in E_{a}\Rightarrow
e_{b,a,-}\in\alpha(u_{a,-})$.

Let $S$ be a configuration over $S$. We define the monotone function
$f^{\prime}_{a}$ over the set $\\{s,s^{-}\mid s\in S\\}$ that for every
configuration $x$ verifies $f_{a}(x)=f^{\prime}_{a}(x\sqcup s^{-}\mapsto\neg
x(s))$. The existence of such a function is given by Lemma 2.

For $x^{\prime}$ a configuration over $T_{a}$, and $i$ a configuration over
$E_{a}$, We define $M_{a}(u_{a,+})$ as a function that verifies :

$M_{a}(u_{a,+})(x^{\prime}\sqcup i)=\\\ f^{\prime}_{a}(a\mapsto
x^{\prime}(u_{a,+})\sqcup a^{-}\mapsto
x^{\prime}(u_{a,-})\sqcup\bigsqcup\limits_{b\neq a}\left(b\mapsto
i^{\prime}(e_{b,a,+})\sqcup b^{-}\mapsto i^{\prime}(e_{b,a,-})\right))$

The function $M_{a}(u_{a,-})$ is given by $M_{a}(u_{a,-})(x^{\prime}\sqcup
i)=\neg M_{a}(u_{a,+})(x^{\prime}\sqcup i)$.

This local module is composed of two automata, one that computes the original
function and one that computes the negation of the original function. This
allows us to simulate the original network while being locally monotone. The
monotony is given by the fact that the configurations used for simulation are
now incomparable to each other. A representation of an example is presented in
Figure 8.

$u_{a,+}$$u_{a,-}$$f_{a}(x)$$\neg
f_{a}(x)$$e_{b,a,+}$$e_{c,a,+}$$e_{b,a,-}$$e_{c,a,-}$ Figure 8: Interaction
graph of the locally monotone module for the example function
$f_{a}(x)=x_{a}\wedge(\neg x_{b}\vee x_{c})$. As $x_{a}$ is present in the
local function, the two automaton composing this module loop between each
other and themselves.

We define $U_{b,a}$ such that $U_{b,a}=T_{a}$ if the variable $x_{b}$ is
included in function $f_{a}$, and $U_{b,a}=\varnothing$ otherwise.

The encodings $\phi_{a}$ and $\phi_{b,a}$ for every $b$ such that
$U_{b,a}\neq\varnothing$ are defined by :

$\phi_{a}(x^{\prime})=\phi_{b,a}(x^{\prime})=\begin{array}[]{\\{}{ll}.1&\text{if
}x^{\prime}(u_{a,+})=1\text{ and }x^{\prime}(u_{a,-})=0\\\ 0&\text{if
}x^{\prime}(u_{a,+})=0\text{ and }x^{\prime}(u_{a,-})=1\\\
\bullet&\text{otherwise}\end{array}.$

For every $b$ such that $U_{b,a}\neq\varnothing$, we define
$I_{b,a}(e_{b,a,+})=u_{b,+}$ and $I_{b,a}(e_{b,a,-})=u_{b,-}$. In other words,
the positive (resp. negative) value of automaton $b$ is given by the value of
the positive (resp. negative) node of the local module $M_{b}$.

###### Lemma 3

$M_{a}$ locally simulates $f_{a}$ in a input-first way.

Let $\Delta_{a}=\\{T_{a}\\}$ be an input-first way update mode for the module
$M_{a}$. Let $x$ be a configuration over $F$. Let $x^{\prime}$ be a
configuration over $T_{a}$ such that $\phi(x^{\prime})=x_{a}$. Let
$i^{\prime}$ be an input configuration over $E_{a}$ such that for any $b\neq
a$, $\phi_{b,a}(i^{\prime}\circ I^{-1}_{b,a})=x_{b}$.

Such a $x^{\prime}$ verifies $x^{\prime}(u_{a,+})=x_{a}$ and
$x^{\prime}(u_{a,-})=\neg x_{a}$. Such a $i^{\prime}$ verifies
$i^{\prime}(e_{b,a,+})=x_{b}$ and $i^{\prime}(e_{b,a,-})=\neg x_{b}$ for every
$b\neq a$. Theses configurations are well defined.

To prove Lemma 3, we have to show that
$\phi_{a}(M_{a\Delta_{a}}(x^{\prime}\sqcup i^{\prime}))=f_{a}(x)$. This is
equivalent to :

$\Leftrightarrow\begin{array}[]{\\{}{ll}.M_{a}(u_{+,a})(x^{\prime}\sqcup
i^{\prime})=f_{a}(x)\\\ M_{a}(u_{-,a})(x^{\prime}\sqcup i^{\prime})=\neg
f_{a}(x)\end{array}$

$\Leftrightarrow\begin{array}[]{\\{}{ll}.M_{a}(u_{+,a})(x^{\prime}\sqcup
i^{\prime})=f_{a}(x)\\\ \neg M_{a}(u_{+,a})(x^{\prime}\sqcup i^{\prime})=\neg
f_{a}(x)\end{array}$

$\Leftrightarrow M_{a}(u_{+,a})(x^{\prime}\sqcup i^{\prime})=f_{a}(x)\\\
\Leftrightarrow f^{\prime}_{a}(a\mapsto x^{\prime}(u_{a,+})\sqcup a^{-}\mapsto
x^{\prime}(u_{a,-})\sqcup\bigsqcup\limits_{b\neq a}\left(b\mapsto
i^{\prime}(e_{b,a,+})\sqcup b^{-}\mapsto i^{\prime}(e_{b,a,-})\right))\\\
=f_{a}(x).$

We noticed earlier that $x^{\prime}(u_{a,+})=\neg x^{\prime}(u_{a,-})$ and
that $i^{\prime}(e_{b,a,+})=\neg i^{\prime}(e_{b,a,-})$ for every $a\neq b$.
This implies that our this evaluation of $f^{\prime}_{a}$ can be developed as
follows :

$f^{\prime}_{a}(a\mapsto x^{\prime}(u_{a,+})\sqcup a^{-}\mapsto
x^{\prime}(u_{a,-})\sqcup\bigsqcup\limits_{b\neq a}\left(b\mapsto
i^{\prime}(e_{b,a,+})\sqcup b^{-}\mapsto i^{\prime}(e_{b,a,-})\right))\\\
=f_{a}(a\mapsto x^{\prime}(u_{a,+})\sqcup\bigsqcup\limits_{b\neq a}b\mapsto
i^{\prime}(e_{b,a,+}))=f_{a}(a\mapsto x_{a}\sqcup\bigsqcup\limits_{b \neq
a}b\mapsto x_{b})\\\ =f_{a}(x),$

which concludes the proof of the Lemma 3. Using this lemma, knowing that the
Lemma 2 implies the monotony of each function in the local modules and the
simple fact that local monotony is not broken by any wiring, we use Theorem
6.1 to conclude this proof.∎