Franck Delaplace
email: franck.delaplace@ibisc.univ-evry.fr

Sergiu Ivanov
email: sergiu.ivanov@ibisc.univ-evry.fr

Bisimilar Booleanization of Multivalued Networks

Keywords: Boolean Network, multivalued network, Bisimulation, Biological network modelling, Automatic conversion inference

Discrete modelling frameworks of Biological networks can be divided in two distinct categories: Boolean and multivalued. Although multivalued networks are more expressive for qualifying the regulatory behaviours modelled by more than two values, the ability to automatically convert them to Boolean network with an equivalent behaviour breaks down the fundamental borders between the two approaches. Theoretically investigating the conversion process provides relevant insights into bridging the gap between them. Basically, the conversion aims at finding a Boolean network bisimulating a multivalued one. In this article, we investigate the bisimilar conversion where the Boolean integer coding is a parameter that can be freely modified. Based on this analysis, we define a computational method automatically inferring a bisimilar Boolean network from a given multivalued one.

Introduction

Discrete network based modelling frameworks, seminally introduced by S. Kauffman [START_REF] Glass | The logical analysis of continuous, non-linear biochemical control networks[END_REF][START_REF] Kauffman | Metabolic stability and epigenesis in randomly constructed genetic nets[END_REF] and R. [START_REF] Thomas | Behaviour of Biological Biological Role of Feedback Loops and Practical Use of the Concept of the Loop-Characteristic[END_REF][START_REF] Thomas | Behaviour of Biological Biological Role of Feedback Loops and Practical Use of the Concept of the Loop-Characteristic[END_REF] for regulation network modelling can be divided in two distinct categories: Boolean networks and multivalued networks. In the former, the states of genes are modelled by Boolean values, with propositional logic as the modelling framework, whereas in the latter the state is extended to the integer domain, also called multivalued, using Presburger arithmetic as modelling framework. It is often admitted that multivalued networks provide more expressiveness for modelling gene expression behaviour by distinguishing between more than two states (i.e., off or on) for specifying the regulatory activity. However, the ability to automatically convert a multivalued network to a Boolean one with the same dynamical behaviour weakens this distinction from an analytical standpoint since the analysis of the dynamics can be performed on the Boolean network directly.

More generally, the Boolean conversion of a multivalued network offers the opportunity to bridge the gap between the two modelling formalisms that enables to inherit, adapt and extend the theoretical results defined in a framework to the other [START_REF] Tonello | On the conversion of multivalued to Boolean dynamics[END_REF]. Moreover, this allows the use of software based on propositional logic that could prove computationally more efficient than the algorithms developed for Presburger arithmetic for the same problem. In particular, a wide spectrum of problems in modelling regulatory networks by symbolic characterization of stable states can be formalized as problems of logical valuation of variables satisfying a formula in the Boolean case (the SAT problem) or finding solutions complying to a set of linear constraints for the integer case (integer linear programming, ILP). [START_REF] Aloul | Generic ilp versus specialized 0-1 ilp: An update[END_REF] provide an experimental comparison of ILP and SAT solvers applied to the SAT problem.

By considering these opportunities, the issue is thus to investigate methods for converting multivalued networks to Boolean while preserving the dynamical behaviour. This conversion is primarily based on an encoding of integers by Boolean profiles, establishing the equivalence between the two kinds of values. The challenge is to extend this equivalence to state transitions in order to certify the behavioural integrity.

In [START_REF] Didier | Mapping multivalued onto boolean dynamics[END_REF], G. Didier, E. Remy and C. Chaouiya extensively study the conditions for the conversion of multivalued networks to Boolean ones using Van Ham code (Van Ham, 1979) (Section 4). To overcome the potential limitation of Van Ham code restraining the dynamics to a sub-region of the Boolean state space, A. Fauré and S. Kaji study the conversion based on Summing code (Section 4), which provides several alternative Boolean profiles for encoding an integer, such that the resulting Boolean dynamics is deployed on the whole Boolean state space [START_REF] Fauré | A circuit-preserving mapping from multilevel to Boolean dynamics[END_REF]. Following similar motivations, E. Tonello also studies the conversion based on this code [START_REF] Tonello | On the conversion of multivalued to Boolean dynamics[END_REF]. Regarding conversion tool, A. Naldi developed the Java library biolqm [START_REF] Naldi | Biolqm: a java toolkit for the manipulation and conversion of logical qualitative models of biological networks[END_REF], which is a toolkit dedicated to qualitative analysis of biological regulatory networks, and which includes a multivalued to Boolean converter. The converter is based on Van Ham coding and ensures that the trajectories always converge to the region of the valid Boolean codings, called the admissible region (Section 3), thereby avoiding potential spurious equilibria outside this region. This converter is also available in ginsim 3.0 environment [START_REF] Chaouiya | Logical modelling of gene regulatory networks with ginsim[END_REF], which relies on biolqm.

These research works elegantly pave the formal foundation of the multivalued to Boolean network conversion. However, the results are intrinsically dependent on a specific coding, the Summing and Van Ham code. Moreover they are mainly designed for the asynchronous mode. Therefore, it appears interesting to generalise this approach by distinguishing the properties that purely relate to the conversion process from those depending on the code for highlighting the foundations of this process.

The behavioural equivalence is formally defined by the reachability preservation property, namely: whenever an integer state is reachable from another one, the equivalent Boolean state of the former is also reachable by the equivalent Boolean state of the latter, and conversely. Reachability preservation relies on the existence of a bisimulation [START_REF] Sangiorgi | Introduction to bisimulation and coinduction[END_REF] between both networks, parametrised by the Boolean-to-integer coding. While preserving the reachability is essential, it also appears desirable to extend the preservation to structural properties of the interactions and other properties related to equilibrium. In this article, we study the network conversion by regarding it as a bisimulation process applied to any Boolean coding of the integers. Based on this study, we propose an algorithm inferring the formulas of a Boolean network behaviourally equivalent to the input multivalued network.

After recalling the main notions of multivalued networks (Section 2), we examine the bisimulation properties between the dynamics of the networks and the admissibility conditions for stating a bisimulation between a multivalued and Boolean networks (Section 3) with regard to different codings (Section 4). Then, we study the extension of the properties preserved by conversion (Section 5). Finally we define a method inferring a Boolean network bisimilar to the multivalued one whatever the coding procedure (Section 6).

We use the following notations:

Set. The complement of a subset EzE I , E I E is denoted by ¡E I . A singleton teu is denoted by its element e.

pY Ñ td i | 0 ¤ d i ¤ Luq. The restriction/projection of a state s D Y on W Y is denoted s W D W .
This notation also holds for function on states, i.e., dom g W D W . A substitution within a state s is the replacement of the value of a variable of s by another value, formally defined as: s ryÞ Ñvs szty Þ Ñ s y u ty Þ Ñ vu. The distance on states is defined as: dps, s I q °n i1 |s y i ¡ s I y i |.

multivalued networks

A multivalued network xg, Y y defined on a set of variables Y is a dynamical system characterized by an evolution function g.

Let L tL i N | 1 ¤ i ¤ nu, n
|Y | be an indexed set of integral values (levels), we define: L Y n i1 L i y i as the product of finite multivalued state domains. The evolution function on this domain g : L Y Ñ L Y is composed of a collection of local evolution functions g pg 1 , ¤ ¤ ¤ , g n q such that g i : L Y Ñ L i y i is defined as follows (see Figure 1 for an example): g i psq 6 9 9 9 9 9 9 9 9 9 9 9 8 9 9 9 9 9 9 9 9 9 9 9 7

1 if C 1 psq 2 if C 2 psq ¤ ¤ ¤ l if C l psq ¤ ¤ ¤ L i if C L psq 0 otherwise (1)
where C l is the guard of level l such that all the guards are mutually exclusive, namely:

ds L Y , d 1 ¤ l, l I ¤ L i : l $ l I ùñ 2pC l psq C l I psqq.
Hence, the application g i psq equals level l if and only if the guard C l psq is satisfied, and by convention 0 is returned when no guards are satisfied.

Model of dynamics. The model of dynamics of a multivalued network xg, Y y is formalized by a labelled transition system x L Y , M, ÝÑ g y where the labels are sets of variables that determine which variables are updated jointly during a transition. The mode M 2 Y describes the organization of the joint updates per transition. For example, in the asynchronous mode, 1 Y tty i uu y i Y , the state of one variable only is updated per transition and in the parallel or synchronous mode tY u, all the variables are updated together.

The mode is also introduced in the network specification if needed, i. Multivalued network is subjected to properties distinguishing the evolution behaviour capabilities. Specifically, the dynamics in which transitions modify the current level by 1 only (i.e., ds ÝÑ s I , dy i Y : dps y i , s I y i q ¤ 1) is said unitary stepwise.

Equilibrium. A state s is an equilibrium, if it can be reached1 infinitely once met:

ds I N Y : s ÝÑ ¦ s I ùñ s I ÝÑ ¦ s.
(

) 2
An attractor is a set of equilibria that are mutually reachable and a stable state is an attractor of cardinality 1. Figure 1 shows an example of a multivalued network and the resulting dynamics for the asynchronous mode with two stable states that are respectively 13 and 00. g 6 9 9 9 9 9 9 9 9 9 9 9 8 9 9 9 9 9 9 9 9 9 9 9 7 Interaction graph. An interaction graph xY, y portrays the interdependencies of the variables in the network xg, Y y. An interaction y i y j exists whenever changing the value of y i may lead to a change in the value of y j :

y i y j def
hs, s I N Y : s y i $ s I y i s ¡y i s I ¡y i g j psq $ g j ps I q.

(3) The signed interaction graph xY, , σy refines the nature of the interac- tions by signing the arcs with σ : p q Ñ t¡1, 0, 1u to represent a monotone relation between the source and target variables of the interaction (4); either increasing (label 1, denoted I I ), or decreasing (label ¡1, denoted I ¡ I ), or neither (label 0, denoted I ¨I), and formally defined as:

y i y j def y i y j ds, s I N Y : s y i ¤ s I
y i s ¡y i s I ¡y i ùñ g j psq ¤ g j ps I q y i ¡ y j def y i y j ds, s I N Y : s y i ¤ s I y i s ¡y i s I ¡y i ùñ g j psq ¥ g j ps I q (4)

Network bisimulation

By definition [START_REF] Sangiorgi | Introduction to bisimulation and coinduction[END_REF], bisimulation between the dynamics of networks preserves the reachability, thereby maintaining the trajectories and the attractors in both ways. Definition 1 illustrated in Figure 2 dw, w I dom ψ, dm M X : w m ÝÑ f w I ùñ ψpwq µpmq ÝÑ g ψpw I q;

2. (backward simulation) for any two multivalued states s, s I L Y , for any w B X such that ψpwq s, and for any n M Y , s n ÝÑ g s I implies that there exists a w I B X and an m M X such that ψpw I q s I , µpmq n and w m ÝÑ f w I : ds, s I L Y , dw B X , dn M Y : ψpwq s s n ÝÑ g s I ùñ hw I B X , hm M X : µpmq n ψpw I q s I w m ÝÑ f w I ¨. Two networks B and N complying with Definition 1 with respect to ψ are said bisimilar, noted B ψ N . Although, (1.2) and (1.1) are similar in their definition, it is worth noticing that they however differ in the following point: all the transitions on the integer state space should fulfill (1.2) whereas only the transitions defined on the domain of ψ, dom ψ, should comply with (1.1). dom ψ circumscribes the admissible region [START_REF] Fauré | A circuit-preserving mapping from multilevel to Boolean dynamics[END_REF][START_REF] Tonello | On the conversion of multivalued to Boolean dynamics[END_REF], where each Boolean state encodes an integer state and each transition is bisimilar to a multivalued one. Hence, no transitions from a state located in the admissible region can escape from this region, thus avoiding aberrant cases exemplified in [START_REF] Tonello | On the conversion of multivalued to Boolean dynamics[END_REF]. From (1.2), we deduce that ψ is a surjective partial function defined on B X but it is not necessary injective and thus not bijective. Hence, the preimage of an integer state is a set:

ψ ¡1 psq tw B X | ψpwq su.
The issue is to determine the conditions on a Boolean network enabling a bisimulation with a multivalued network. These conditions depend on a general relation between the integer and Boolean function including the mode.

From global to local bisimulation discovery

Integer states are coded by the Boolean states in which the Boolean variables storing the code constitute the support of the integer variables. The support function associates each subset of integer variables to its support: p ¤ : 2 Y Ñ 2 X . This function has the following properties: 1) the Boolean variables are exactly the supports of the integer variables, 2) the supports are pairwise disjoint, and 3) they are modular in the sense that the union of the supports is the support of the union of the integer variables: 1q X p Y and, 2q dy i , y j Y : y i $ y j ðñ p y i p y j r and,

3q dY I , Y " Y : { Y I Y " x Y I x Y ". (5)
For example, the state s py 1 ,y 2 q p0, 1q is encoded by w p00, 01q by using the classical binary code or the Gray code. The variables of the Boolean network will be therefore the variables supporting the Boolean code of the integer variables of Y (X p Y ). The states of Boolean variables are respectively: w x y 11 0, w x y 12 0, w x y 21 0, w x y 22 1. Note that there are two kinds of indices: one for the multivalued variables, and the other for the Boolean variables of the corresponding supports. We consider henceforth that ψ fits all supports, i.e.,

ψ ¤ W Y B x W Ñ L W ¨.
The function ψ transforms the Boolean state of the support into an integer state in a modular manner, by decoding distinct sub-parts of a Boolean state separately, so that the decoding of the whole integer state is the union of the local decoding results:

dW Y, dw B p Y : ψpw x W q ψpwq W . (6)
From (5,6) we deduce the following relation on two disjoint sets of variables representing the modularity of the decoding:

ψpw { W W I q ψpw x W qψpw y W I q ψpwq W ψpwq W I, W W I r, W, W I Y.
Moreover, the mode of the converted Boolean network must be compatible with the modularity of the coding. A mode is local-to-support when the parallel updates of the Boolean variables operate inside supports only, namely M is local-to-support if and only if: dm M, hy i Y : m p y i . The asynchronous mode is always local-to-support and the parallel localto-support mode update all the support variable in parallel: tp y i u y i Y . The parallel mode for the Boolean network is not local-to-support since the joined update is accross all the supports. Within the framework, inferring a Boolean network bisimilar to a multivalued one is reduced to the discovery of a Boolean network in bisimulation with a local multivalued network xg i , Y y where only the state of a single variable evolves. A Boolean network in bisimulation with the entire multivalued network results from the union of Boolean networks in bisimulation with local multivalued networks (Proposition 1). Hence, for each g i , we focus on the discovery of the appropriate evolution function of the support f p y i and the determination of the admissible modes for enabling the bisimulation.

Proposition 1. Consider the multivalued network N xg, Y, 1 Y y and the family pB i q y i Y of Boolean networks over the supports of the variables in Y :

B i xf p y i , X, M y i y, M y i 2 p y i .
Then the following holds:

dy i Y : xf p y i , X, M y i y xg i , Y, 1 y i y ¨ùñ xf, X, ¤ y i Y M y i y xg, Y, 1 Y y.
where f pf p y i q y i Y and g pg i q y i Y are the global evolution functions collecting their respective local evolution functions.

According to the definition of a transition (Section 2) and to Proposition 1, for establishing a bisimulation relation between a multivalued transition function f and a Boolean transition function g, it suffices that the local integer evolution function applied to the decoding g i ¥ψpwq coincide with the Boolean evolution function ψ ¥ f p y i pwq or, more generally, with the evolution taken under a local-to-support mode:

ψ ¥ f g ¥ ψ Global function ψpf m pwq w p y i zm q g i ¥ ψpwq, m p y i Local-to-support mode (7)
If ψ is a bijective function then ( 7) is expressed as f ψ ¡1 ¥ g ¥ ψ, which corresponds to the conjugated evolution function defined in [START_REF] Didier | Mapping multivalued onto boolean dynamics[END_REF].

Theorem 1 shows that Property ( 7) is necessary and sufficient to ascertain that a multivalued network bisimulates a Boolean network with a local-tosupport mode.

Theorem 1. Let N xg i , Y, 1 y i y be a multivalued network, B xf p y i , p
Y , M y a Boolean network with M a local-to-support mode, and ψ : B p

y i Ñ L y i , a
surjective function, Property 7 is met between the evolution functions of B and N if and only if B ψ N .

Bisimulation admisibility

The bisimulation necessitates to comply with conditions involving the mode and the coding. In this section we focus on the admissibility condition for the bisimulation extending the result of Theorem 1.

Admissibility based on mode and coding. The mode may prevent the bisimulation by forbidding the implementation of a Boolean transition simulating a multivalued transition. For example, assume that g i p0q 2 leading to the multivalued transition 0 y i ÝÑ 2, the Boolean transition simulating it is naturally 00

w p y 1 ,w p y 2
ÝÑ 11 using the Gray code or any coding procedures detailed in Section 4. However, this Boolean transition cannot be implemented in the asynchronous mode because both variables of the support should be updated jointly which is prohibited by the mode policy. Now, assume that the binary code is used leading to the Boolean transition 00

w p y 1 ,w p y 2
ÝÑ 10 then the asynchronous Boolean transition is enabled by updating the first Boolean support variable (w p y 1 ) only. Hence, the mode selection strongly depends on a relation between the mode and the coding. Therefore the primary admissibility condition for the bisimulation lies on the mode selection of the Boolean network with regards to the coding that should enable the simulation for all multivalued transitions considered independently. Formally, a transition of a Boolean network B xf, W, M y always fulfils: dw, w I B W , dm M : w m ÝÑ w I ùñ dpw, w I q ¤ |m|.

Otherwise, the transition cannot be implemented due to the number of modifications exceeding the permitted capacity offered by the mode. The permissible distance for enabling a transition has connexion with the distance on Boolean coded integers. All the codings ψ described in Section 4 fulfil the condition stipulating that the distance between multivalued states is always lower or equal to the (Hamming) distance of their Boolean code:

ds y i , s I y i L i y i : ψpw p y i q s y i , ψpw I p y i q s I y i ùñ dps y i , s I y i q ¤ dpw p y i , w I p y i q.
Thereby, if a Boolean network B bisimulates a multivalued network N xg i , Y, 1 y i y, we deduce from these two previous properties that:

ds L Y , dw, w I B p Y , dm M :
ψpw p y i q s y i ψpw I p y i q g i psq w m ÝÑ w I ùñ dps y i , s I y i q ¤ dpw, w I q ¤ |m|.

This property characterizes the unique necessary bisimulation admissibility condition with regards to a local-to-support mode used for Boolean network and the codings of Section 4. An admissibility test can be finally derived establishing a condition between the multivalued network and the mode of the Boolean network directly:

ds L Y , dy i Y : dps y i , g i psqq ¤ mint|m| | m M u. ( 8
)
As practical consequence, the local-to-support parallel/synchronous mode enables the bisimulation with any multivalued network and only the unitary stepwise multivalued network (Section 2) can be bisimulated by asynchronous Boolean network since the cardinality of the modalities is always 1.

Family of admissible bisimilar Boolean networks. Theorem 1 states the equivalence between bisimilarity and Property 7 for local-to-support modes. we extend this result to a larger family of modes that are admissible with respect to the parallel mode. Informally, a modality m is m 0 -admissible if, for any Boolean state w, running f on w under m or under m 0 yields (possibly different) states belonging to the same preimage under ψ. Definitions 2 and 3 detail this compatibility formally. Both definitions assume the Boolean network B xf, p Y , M 0 y operating in mode M 0 and the multivalued network N xg i , Y, 1 y i y. Definition 2. A mode component m M is m 0 -admissible with respect to the functional bisimulation B 0 ψ N denoted by adm ψ pm, m 0 q, if the following holds: 1. dm 0 M 0 , hm M : adm ψ pm, m 0 q; 2. dm M, hm 0 M 0 : adm ψ pm, m 0 q.

dw B p Y : ψpf m 0 pwq w ¡m 0 q ψpf m pwq w ¡m q. w w I w P f m 0 f m ψpwq ψpw I q ψpw P q ψ ψ
According to the definition, a mode M is M 0 -admissible if, for every modality m M , there exists a modality m 0 M 0 such that m is m 0admissible. Note that this requirement does not imply the existence of a bijection between M and M 0 : two functions M 0 Ñ M and M Ñ M 0 are indeed required by, respectively, clauses (1) and (2) of Definition 3, but they may not be each other's inverses.

Lemma 1. The relation of admissibility with respect to the functional bisimulation B ψ N , defined on all possible modes of B, is an equivalence relation.

Intuitively, two modes are admissible with respect to a functional bisimulation ψ if the application of ψ to the transitions in both dynamics leads to the same dynamics that corresponds to the dynamics of N . This implies that admissible modes cannot be distinguished with respect to the bisimulation relation. The following theorem formally captures this observation.

Theorem 2. Given the functional bisimulation B ψ N between the Boolean network B xf, p Y , M 0 y and the multivalued network

N xg i , Y, 1 y i y, any Boolean network B I xf, p
Y , M y with adm ψ pM, M 0 q functionally bisimulates N as well:

dM 2 p Y : B ψ N adm ψ pM, M 0 q ùñ B I ψ N. N xg i , Y, 1 y i y B xf, p Y , M 0 y B I xf, p Y , M y ψ ψ adm ψ pM, M 0 q

Boolean coding

The coding procedure characterizes a function ψ mapping a Boolean profile to an integer. We study two fundamental codes that are suitable for asynchronous Boolean dynamics: the Summing code and the Gray code. Table 1 shows both codings for encoding levels ranging from 0 to 3. Summing code. For the Summing code, the integer is the sum of the states of the Boolean support variables:

ψpw p y i q p y ik p y i w p y ik .
The size of the support is linear in the maximal level, |p y i | L, and different encodings are possible for the same integer. The number of different codes for an integer 0 ¤ l ¤ L is L l ¨. Van Ham code (Van Ham, 1979) is a sub-case of the Summing code in which the unitary stepwise evolution restricts the filling of 1 from left to right. The van Ham code is emphasized in bold in Table 1.

Gray code. The Gray code associates Boolean states differing in only one position to consecutive integers. The coding function is bijective and constructs the integer value from a Boolean state by first transforming a Gray code profile into its equivalent binary code and then by computing the integer from this coding 2 :

ψpw p y i q | p y i | ķ1 2 | p y i |¡k . k à j1 w p y ij .
The support size is logarithmic in the maximal level:

|p y i | rlog 2 pL 1qs.
The Summing code is defined on the whole Boolean state space (i.e.,

dom ψ B p Y ).
The Gray code can be also defined on the whole Boolean space 2 `is the exclusive or, xor.

0 1 2 3 p0, 1, 0q p1, 1, 0q
p0, 0, 0q p1, 0, 0q p0, 1, 1q p1, 1, 1q p0, 0, 1q p1, 0, 1q

-Summing code - p0, 0q p0, 1q p1, 1q p0, 1q
-Gray code - when the maximal number of levels is L 2 k ¡1. The Van Ham code, on the other hand, never covers the entire Boolean space, except when the maximal level is 1 corresponding to Boolean. All these codings associate the integer 0 to the 0 Boolean profile. Furthermore, they all fulfil the neighbourhood preserving property (9) defined in [START_REF] Didier | Mapping multivalued onto boolean dynamics[END_REF] and stressing that the distance of 1 between two integer states should map to a distance of 1 between the corresponding Boolean states, and conversely:

ds, s I L Y : dps, s I q 1 ùñ hw ψ ¡1 psq, hw I ψ ¡1 ps I q : dpw, w I q 1 dw, w I dom ψ : dpw, w I q 1 ùñ dpψpwq, ψpw I qq 1.

(9)

These codes are individual representatives of families of linear and logsize codes which can be obtained by a permutation π on the integer states, i.e., ψ I π ¥ ψ. This permutation may notably relax the neighbourhood preserving property. In literature, the study of the multivalued-to-Boolean network conversion has been carried out extensively for Summing and Van Ham codes [START_REF] Didier | Mapping multivalued onto boolean dynamics[END_REF][START_REF] Fauré | A circuit-preserving mapping from multilevel to Boolean dynamics[END_REF][START_REF] Tonello | On the conversion of multivalued to Boolean dynamics[END_REF] but not Gray code which provides the most compact binary representation of integers and may be bijective.

Extensions of property preservation

Although bisimulation preserves the essential property of reachability, it appears desirable to preserve additional properties for performing an accurate analysis of dynamics on the Boolean network directly. These additional properties pertain to the nature of equilibria and the interaction graph.

Preservation of stability of the equilibria

By definition of the bisimulation, the equilibria of a multivalued network match with the equilibria of a bisimilar Boolean network, and conversely. However, when some equilibria are stable states, their nature may differ: a stable state of the multivalued network can be represented by a cyclic attractor over Boolean profiles, all coding for the same integer (Figure 5). Nevertheless, any cyclic attractor will still be bisimulated by a cyclic attrac- tor since, by definition of coding, a transition between two different integer states is always simulated by a transition with two different Boolean profiles. Figure 5 shows an example where the self-loop of stable state 2 is simulated by a cyclic attractor over the three Boolean profiles coding for it (right-hand side network). Indeed, for any integer level, the synchronous dynamics allows reaching any of its codings from any other one. This case is however not encountered for stable state 3 coded by a single Boolean profile. The occurrence of such situations also depends on the concrete Boolean function, as shown by the middle network that preserves the stability. Even though in the former case the stable state is represented by a cyclic attractor, it is worth noticing that the original level 2 can be recovered from the states encompassed by the attractor since tψp101q, ψp011q, ψp110qu t2u.

Maintaining the stability matters for the analysis performed on the Boolean dynamics. In particular, the symbolic computation of stable states will fail to find state 2 as equilibrium from the Boolean network since this state is represented by a cyclic attractor. Therefore, such cases should be ruled out to ensure a matching analysis of the dynamics on the two networks. To preserve the stability of equilibria, we basically have to prevent reaching a code of an integer level l from another code also encoding for l. This depends on the mode and on the Boolean function (cf. Figure 5). The expected outcome can be expressed as follows for a mode M : dw dom ψ, dm M : w m $ f m pwq ùñ ψpwq $ ψpf m pwq w ¡m q. (10)

We examine two effective conditions for satisfying (10) that are independent of the specification of the Boolean network. A simple one working whatever the mode and the Boolean function is to remove the self-loops, and thus establish bisimulation between reflexive reductions of the state graphs of both networks, instead of operating on the original state graphs. The equilibrium stability then remains preserved since no circuits can simulate a self-loop and the important features of the reachability are not altered. Another more explicit condition, based on the code and the cardinality of modalities, forbids the access by a transition to another Boolean profile coding for the same integer. dy i Y, ds y i L y i , dw, w I ψ ¡1 ps y i q :

w $ w I ùñ dpw, w I q ¡ maxt|m| | m M u, then the equilibrium stability (10) is preserved.

Consequently, if ψ is a bijection, the stability of equilibria is preserved since every integer level is coded by a single Boolean profile. On the other hand, the asynchronous mode preserves the stability under the Summing code, since distances between two Boolean profiles coding for the same integer are at least 2.

Interaction preserving

A Boolean network bisimulating a multivalued network is regulatorypreserving if it is possible to unambiguously recover the signed interaction graph of the multivalued network (migs), xY, , σy, from the signed Boolean interaction graph of the bisimilar Boolean network (bigs), x p Y , , σ B y.

Retrieving migs from bigs is divided in two steps: retrieving the interaction graph and finding the signs.

Interaction graph retrieval. The structure of migs is retrieved from the quotient graph of bigs defined on the support of the integer variables, called the support interaction graph (sig) xtp y i u y i Y , y, where an interaction between two Boolean support variables induces an interaction between the supports they belong:

As a consequence, the topological structure of migs is the same as that of sig by merely replacing the supports by the integer variables they support (Proposition 3). In fact, sig essentially provides an intermediary representation used for recovering the interactions of migs and their signs.

Proposition 3. Let N be a multivalued network and B a Boolean network.

If N is bisimilar to B then migspN q is isomorphic to sigpBq.

Sign retrieval. The sign of an interaction is determined by bigs once the conversion is achieved (see Figures 6,7). Therefore the issue is to deduce from the signs of the interactions between the Boolean variables the signs of the corresponding interactions in migs. The recovery procedure is based on a set of reference Boolean variables, considered as markers of sign, covering all the supports such that the signs of the interactions between these variables are the same as the signs of the interactions between the integer variables they support. Y is a set of markers of sign if and only if:

1. The sign σ of an interaction between any two Boolean variables in

M p Y p
Y is the same as the sign of the interaction between the integer variables that they support:

dp y i k , p y j r M p Y : p y i k σ p y j r ðñ y i σ y j .
2. All integer variables have markers:

dy i Y : M p Y p y i $ r.
To operationally identify the markers from a code, we define a codebased marker condition ( 12) directly linking the markers to the code for the asynchronous mode. This condition asserts the monotony of the coding for markers with respect to the integer and Boolean orders by stipulating that an integer coded by a Boolean profile is less than another coded by this Boolean profile where a marker value is substituted by 1 (Lemma 2). Y be a set of Boolean variables complying to (4.2). If:

dp y i k M p Y , dw dom ψ : ψpwq ¤ ψpw r p y ik Þ Ñ1s q (12)
then M p Y fulfils Definition (4.1) and M p Y is a set of markers.

Therefore, the goal is to determine for each integer variable the set of markers by checking (12) for a given coding. For the Summing code all the Boolean variables are markers, and for the Gray code the variables storing the most significant bit indexed by 1 ( p y i 1 ) are the markers. Gray code:

M p Y tp y i 1 | y i Y u.

Inference of Boolean formulas

An analytical definition of the Boolean network function is given by ( 7).

Although the function ψ ¡1 ¥ g ¥ ψ is closed on Boolean states when ψ is bijective characterizing a Boolean network, the Boolean formulas are not explicitly defined. The lack of Boolean formulas makes the analysis harder in practice, notably by preventing the characterization of the interaction graph directly from formula specifications. Moreover, the analytical definition does not hold when ψ is not bijective, since ψ ¡1 returns a set of Boolean profiles.

To circumvent this limitation, the objective is to infer the Boolean network bisimilar to a multivalued network directly from the specification of the latter (1). As it is sufficient to find a bisimilar Boolean network for each local multivalued evolution function g i (Proposition 1), the algorithm will act on each function of integer variables independently. In this section we define a method inferring the formulas f i,k for each support variable p y i k of y i such that the reflexive reduction of the resulting Boolean network is bisimilar to the reflexive reduction of the initial multivalued network where the code is a parameter of this method. Due to the reflexive reductions, this method preserves the nature of the stable states (Section 5.1). For simplicity, the inference is presented for the asynchronous mode with a unitary stepwise multivalued network as input. However the inference can be applied to any local-to-support mode. This point is discussed at the end of the section.

The definition of a formula f i,k for a support variable is divided in two stages: The conversion of the guard into a Boolean form, and the derivation of the admissibility condition for guard validation. The examples use the Summing code which is the most complex coding for the inference.

Boolean conversion of the guard. Basically, the guard of level l I must also be satisfied in the Boolean network to simulate a transition shifting the current level l to l I . The conversion of a multivalued guard to a Boolean guard gathers the codes of the state profiles fulfilling the conditions of level l I , i.e., C l I y i ts p y i q | C l I psqu where p y i q is the set of regulators of y i . As all these integer states satisfy the guard C l I , their Boolean codes should also satisfy the Boolean guard C l I B defined as3 :

C l I B ª sC l I y i ¤ ¥ © y j p y i q ª w x y j ψ ¡1 psy j q mintermpw x y j q . ( 13
)
For example, in the case of the multivalued network from Figure 1, the states fulfilling the conditions to reach level 2 for y are px 1, y 1q for the transition from level 1 to 2 for y, or px 0, y 3q for the transition from level 3 to 2. The code for x is ψ ¡1

x p0q tp0qu, ψ ¡1

x p1q tp1qu and the codes for y are respectively for 1 and 3: ψ ¡1 y p1q tp0, 0, 1q, p0, 1, 0q, p1, 0, 0qu and ψ ¡1 y p3q tp1, 1, 1qu. Hence, the Boolean guard of level 2 for y is:

C 2 B px1,y1q ¤ ¦ ¥ p x lo omo on mintermxp1q ¤ ¦ ¥pp y 1 2p y 2 2p y 3 q looooooooooomooooooooooon mintermyp1,0,0q p2p y 1 p y 2 2p y 3 q looooooooomooooooooon mintermyp0,1,0q p2p y 1 2p y 2 p y 3 q looooooooomooooooooon mintermyp0,0,1q px0,y3q ¤ ¦ ¥ 2p x lo omo on mintermxp0q pp y 1 p y 2 p y 3 q looooooomooooooon mintermyp1,1,1q
Guard admissibility condition. The generation of the Boolean guard is however insufficient for obtaining the final formula because some support variables shift to 0 during the transition even though the guard is satisfied, meaning that a direct evaluation of the Boolean guard would shift them to 1. For example, in Figure 1, shifting from 3 to 2 for y is bisimilar to p1, 1, 1q p y 2 ÝÑ p1, 0, 1q. In this case, we need to shift the state of p y 2 to 0 although the guard is satisfied with s x 0. We thus need to characterize the situations in which the transition necessarily shifts the value of a support still allow reaching a Boolean profile coding for l I by setting p y i k to 0. The resulting transition is bisimilar to an integer transition, and thus must be kept.

The guard admissibility condition G of C l I B is thus defined as the disjunction of the minterms of the admissible codes:

G Ψ Ñ1 pl I , p y ik q ª cΨ Ñ1 pl I , p y ik q mintermpcq. (14)
In our running example, consider the levels that potentially reach level 2 in a unitary stepwise transition (levels 1, 2, and 3). The final simplified formulas of the code admissibility conditions G Ψ Ñ1 p2,p y k q , 1 ¤ k ¤ 3, for each support variable are detailed in Table 2.

From these conditions (Table 2), we deduce that the asynchronous transitions from level 3 coded by p1, 1, 1q to level 2 all set to 0 one of the Boolean support variables. Indeed, the update of p y 1 to 0 leads to p0, 1, 1q and similarly for p y 2 , p1, 0, 1q and p y 3 , p1, 1, 0q that all represent a Summing code of level 2.

G Ψ Ñ1 p2,p y 1 q py 1 2y 2 q py 2 2y 3 q p2y 2 y 3 q G Ψ Ñ1 p2,p y 2 q py 1 2y 3 q p2y 1 y 3 q py 2 2y 3 q G Ψ Ñ1 p2,p y 3 q py 1 2y 2 q p2y 1 y 2 q p2y 2 y 3 q

Table 2: Guard admissibility condition for level 2 of the support variables of y.

Boolean formula of a support variable. The final formula f i,k for a support variable p y i,k can be understood as the Boolean version of the guards restricted to the codings admissible for their triggering, defined as:

f i,k ª 1¤l¤L C l B G Ψ Ñ1 pl, p y ik q ¨.
(15)

The Boolean network gathers the formulas defined by ( 15) for each support variable. For the running example (Figure 1), the final Boolean network provides a clean description of the formulas once simplified for the Summing code (Figure 6) and the Gray code (Figure 7), that differ due to the codings. Theorem 4 demonstrates the correction of the conversion method. Extension to other modes. The method can be applied to any local-to-support mode but the admissible region may be reduced compared to the asynchronous mode. This reduction is caused by the decrease of the update capacity allowed by the mode. Hence, by Definition 1, this implies selecting the appropriate codes for always reaching a code supporting an unitary stepwise transition for each update according to the mode components. For the running example, by using the parallel local-to-support mode with the Summing code, M ttxu, tp y 1 , p y 2 , p y 3 uu, all the Boolean variables of p y are updated jointly allowing to reach a single code instead of reaching the different codes of the same integer by separate updates of variables. Thus, the coding is reduced to Van Ham coding.

Moreover, the trajectories starting from a state located outside the admissible region always end in the admissible region and no supplementary equilibra are thus created (Proposition 4). This property generally holds for any coding that partially covers the Boolean state space.

In conclusion, the domain of ψ may thus be reduced for a surjective decoding function such as the Summing code without altering the asymptotic dynamics, but remains unchanged for a bijective decoding.

dw B p Y , hw I dom ψ : w ÝÑ f w I .
Complexity of the algorithm. Assume that the multivalued network has n variables reaching at most level L, the upper bound on the number of regulators for a variable is r, the maximal number of support variables is m, and the maximal bound of code variants is c. Then the complexity of the Boolean guard is in OpnL r rcmq and the complexity of computing the guard admissibility condition is in OpnLcmq. Thus the complexity of the algorithm is dominated by the complexity of the Boolean guard computation. Accordingly, the computation time mainly depends on the maximal level and the number of regulators. The algorithm is efficient in practice since the maximal level and the number of regulators often remain tractable on real biological network models.

Conclusion

The conversion of multivalued networks to Boolean networks bridges these formalisms by providing a better understanding of the theoretical differences and similarities between these frameworks, and by extending the use of analytical tools dedicated to Boolean networks to their multivalued counterpart. The major property to be preserved at conversion is reachability, ensuring the equivalence between the dynamics. Accordingly, the conversion is underpinned by bisimulation (Section 3) which guarantees the preservation of reachability. The fundamental analysis concludes with an original algorithm that automatically generates a Boolean network bisimulating a multivalued network. The input multivalued network operates under the asynchronous mode, while the resulting Boolean network operates under a local-to-support mode. The proposed framework explicitly distinguishes the conversion process from choosing a Boolean encoding, which separates the properties related to the bisimulation from those related to the encoding, or both.

A number of results relate to the asynchronous mode, which is standard for discrete biological network modelling [START_REF] Thieffry | Dynamical behaviour of biological regulatory networks-ii. immunity control in bacteriophage lambda[END_REF][START_REF] Thomas | Behaviour of Biological Biological Role of Feedback Loops and Practical Use of the Concept of the Loop-Characteristic[END_REF]. Accordingly, our analysis promotes local-to-support modes, which are a natural decomposition of the updates of Boolean variables. Indeed, the joint updates of Boolean support variables should always correspond to a single transition in the multivalued dynamics. Hence, localto-support modes fit well with asynchronous updates of the multivalued variables, facilitating the conversion process.

Even though the preservation of reachability is central for conversion, this property is not sufficient for analysis. Additional properties are also required pertaining to the nature of the equilibria (Section 5.1) and to the interaction graph (Section 5.2). The preservation of stable states ensures that both networks have attractors of the same kind. In particular, this enables a fast symbolic discovery of stable states using SAT solvers. The preservation of stable states needs to depend on the mode and the coding, in order to prevent reciprocal transitions between Boolean profiles coding for the same integer. The asynchronous mode fulfils this property for all codings.

The regulation graph of the multivalued network must also be retrieved from the bisimilar Boolean network. All the codings comply with this property. This property also addresses the issue of monotonicity preservation, because preserving the sign means preserving the transition variation. For Summing and Van Ham codes, the interactions on Boolean variables are all identical to the interactions between the multivalued variables they support. For Gray code, the interaction graph is retrieved from the support variable carrying the most significant bit. Therefore Gray code possibly induces nonmonotonicity for the other support variables as shown in Figure 7.

Accordingly, the choice of the most suitable coding for the conversion depends on several factors which are: the compactness of the coding, the coverage of the Boolean space by the admissible region, the bijection of the (de)coding function ψ, and the monotonicity preservation. A log-size coding with a bijective (de)coding function and a full coverage of the Boolean space preserving the monotonicity would provide a Boolean simulation with the most compact representation, a simple state conversion represented by a conjugated function, without spurious trajectories outside the admissible region, and following the same state variation in each trajectory. However, none of these codings complies with all these requirements at the same time, which introduces a trade-off between the desired preservation properties. Table 3 summarizes these properties for each coding. Such automatic conversion sketches a pipeline where the multivalued network becomes an input specification for modelling while the bulk of the analysis is performed on the Boolean network. Such pipeline suggests that the Boolean framework is central and sufficient for biological network modelling, thus calling to focus theoretical efforts on this framework since the results will benefit to both categories of discrete models via this pipeline.

A research perspective would concern the extension of the bisimulation to other modes for the multivalued network, while considering families of localto-support modes for the Boolean network to fit the multivalued mode. Another perspective may focus on the bisimulation between Boolean networks themselves. As bisimulation formally represents behavioural equivalence, we could investigate the global properties of families of bisimilar Boolean networks in order to discover general rules governing their behaviour. Moreover, given a Boolean network, we may exhibit a simpler bisimilar Boolean network on which the analysis will be performed, and that will potentially improve the efficiency of the dynamics analysis. g i ¥ ψpwq s ¡y i as ψpwq s by hypothesis; ψpf m pwq w p y i zm q s ¡y i from ( 7), true d by hypothesis; ψpf m pwq w p y i zm q ψpw y ¡y i q from (6) and ψpwq s; ψpf m pwq w p y i zm q ψpw ¡ p y i q by definition of the support (5); ψpf m pwq w p y i zm q w ¡ p y i q from (6); ψpf m pwq w p y i zm¡ p y i by definition of the support (5); ψpf m pwq w ¡m q by (T1).

Thus, we conclude that ψpw I q s I implies that w I f m pwq w p In conclusion, if Property 7 is verified then networks N and B are bisimilar with respect to ψ.

p ðù q Assume that N ψ B. Hence, for all transitions w m ÝÑ f w I such that w, w I dom ψ, there exist s, s I L Y such that s ÝÑ g i s I and s ψpwq, s I ψpw I q.

From the bisimulation, we deduce that: s I ψpw I q by hypothesis; ψpf m w ¡m q by definition of w m ÝÑ f w I ; ψpf m w p y i zm¡ p y i q by (T1); ψpf m w p y i zm w ¡ p y i q from (5); ψpf m w p y i zm q ψpw ¡ p y i q by (5), ( 6); ψpf m w p y i zm q s ¡y i as s ψpwq by hypothesis.

From the definition of a transition, we deduce the following:

s I g i psq s ¡y i as s ÝÑ g i s I by hypothesis; g i ¥ ψpwq s ¡y i as s ψpwq by the bisimulation hypothesis.

As ¡y i y i r because ¡y i Y zy i , we can simplify the equation by removing s ¡y i in both part, leading to: ψpf m w p y i zm q g i ¥ ψpwq for all w dom ψ, which defines Property (7).

Lemma 1. That admissibility for modes is reflexive and symmetric follows directly from Definition 3. To show transitivity of admissibility for modes, consider three arbitrary modes M 1 , M 2 , M 3 2 p Y , such that both adm ψ pM 1 , M 2 q and adm ψ pM 2 , M 3 q (with respect to the functional bisimulation B ψ N ).

We can show that clause (1) of Definition 3 is satisfied for modes M 1 and M 3 in the following way: adm ψ pM 1 , M 2 q adm ψ pM 2 , M 3 q ùñ dm 2 M 2 , hm 1 M 1 : adm ψ pm 1 , m 2 q dm 3 M 3 , hm 2 M 2 : adm ψ pm 2 , m 3 q ¨Definition 3 (1) ùñ dm 3 M 3 , hm 2 M 2 , hm 1 M 1 : adm ψ pm 2 , m 3 q adm ψ pm 1 , m 2 q ùñ dm 3 M 3 , hm 1 M 1 : adm ψ pm 1 , m 3 q, where the last transition is done by the symmetricity and transitivity of admissibility for modalities. Showing that clause (2) of Definition 3 is satisfied for M 1 and M 3 can be done symmetrically, which implies adm ψ pM 1 , M 3 q and the transitivity of admissibility for modes. ÝÑ f w P ψpw I q ψpw P q M is M 0 -admissible ùñ hm 0 M 0 , hw P dom ψ ψpwq µpm 0 q ÝÑ g ψpw P q ψpw I q ψpw P q B ψ N ùñ hm 0 M 0 , hw P dom ψ ψpwq µpm 0 q ÝÑ g ψpw I q.

Remark that since N is only allowed to update one variable, y i , µpm 0 q can only be equal to ty i u. Clause (2) (backward simulation): Take any two integer states s, s I L Y and an arbitrary Boolean state w B X . Since N is only allowed to update y i , we can carry out the following deduction: ψpwq s s y i ÝÑ g s I ùñ hw I B X , hm 0 M 0 : µpm 0 q ty i u ψpw I q s I w m 0 ÝÑ f w I B ψ N ùñ hw I B X , hm 0 M 0 , hw P B X , hm M : µpm 0 q ty i u ψpw I q s I w m 0 ÝÑ f w I ψpw P q ψpw I q w m ÝÑ f w P

M is M 0 -admissible ùñ hw P B X , hm M : ψpw P q s I w m ÝÑ f w P . dy i Y, ds y i L y i , dw, w I ψ ¡1 ps y i q : w $ w I ùñ dpw, w I q ¡ maxt|m| | m M u, Y by definition of a mode, the cancellation process terminates at state 0 p Y , which is always in the admissible region since 0 p y i , dy i Y, is the sole code for the integer value 0, regardless of the variable y i .

In conclusion, the trajectories starting from any w B p Y eventually end up in a state in the admissible region dom ψ.

  e., xg, Y, M y. Thus, only the state of the variables in m M can be updated by a transition s m ÝÑ g s I whereas the state of the other variables remains unchanged i.e., s I g m psq s ¡m . A transition that does not change the state, s m ÝÑ g s, is called a self-loop. The global transition relation corresponds to the union of all transition relations labelled by the components of the mode: ÝÑ g mM m ÝÑ g . Hereafter, f : B X Ñ B X , B t0, 1u, always stands for a Boolean function, g : L Y Ñ L Y designates a multivalued/integer function, and Y corresponds to a set of integer variables. w B X represents a Boolean state whereas s L Y a multivalued one.

Figure 1 :

 1 Figure1: A multivalued network with the interaction graph (below) and the asynchronous dynamics (right), with the self-loops removed.

Figure 2 :

 2 Figure 2: Illustration of a bisimulation pψ, µq between a Boolean and a multivalued network. ψ ¡1 psq and µ ¡1 pnq denote the preimages of s and n under ψ and µ respectively.

Figure 3 :

 3 Figure 3: Illustration of m 0 -admissibility adm ψ pm, m 0 q of a mode component m with respect to the bisimulation B ψ N .

Figure 3

 3 Figure3illustrates the implications of Definition 2. Essentially, two mode components are admissible with respect to the bisimulation relation ψ if the image of any Boolean state under these two mode components yields Boolean states which are mapped by ψ to the same multivalued state. Notice that it follows directly from the definition that admissibility is an equivalence relation on mode components. Admissibility can be naturally lifted from mode components to modes: Definition 3. A mode M is M 0 -admissible with respect to the functional bisimulation B ψ N , denoted by adm ψ pM, M 0 q, iff the following conditions hold:

Figure 4 :

 4 Figure 4: Diagrammatic illustration of Theorem 2.

Figure 4

 4 Figure4illustrates the statement of the previous theorem diagrammatically. Given a boolean network B which is functionally bisimilar to a multivalued network N under the mapping ψ, any other Boolean network B I with the same variables and evolution functions as B I , and with an admissi- ble mode with respect to ψ, is also functionally bisimilar to the multivalued network N . Theorem 2 allows us to prove the bisimilarity of a network with another mode provided that Property (7) holds and the mode is admissible.

Figure 5 :

 5 Figure 5: Stability loss during bisimulation -synchronous mode.

Proposition 2 .

 2 Let B xf, p Y , M y be a Boolean network bisimilar to a multivalued network N xg, Y, 1 Y y, with M a local-to-support mode. If the following holds:

Lemma 2 .

 2 Let N xg, Y y be a multivalued network in bisimulation with an asynchronous Boolean network B xf, p Y , 1 p Y y, and M p Y p

Theorem 3 .

 3 Let N xg, Y y be a multivalued network in bisimulation with an asynchronous Boolean network B xf, p Y , 1 p Y y. The sets of markers M p Y are respectively for the codes: Summing code: M p

Figure 6 :

 6 Figure6: A Boolean network bisimilar to the multivalued network in Figure1, its interaction graph (right), and its asynchronous dynamics for the Summing code without the self-loops (below).

Theorem 4 .

 4 Given a neighbourhood preserving Boolean coding ψ such that 0 is coded by the 0 Boolean profile, the inference by (15) from a multivalued unitary stepwise network N xg, Y, 1 Y y produces a Boolean network B xf, p Y , 1 p Y y such that the reflexive reductions of both networks are bisimilar: N $ ψ B $ .

Proposition 4 .

 4 Let f be an evolution function defined according to (15) from a multivalued unitary stepwise network N xg, Y, 1 Y y. Let B xf, p Y , M y be the corresponding Boolean network with M a local-to-support mode, and ψ a decoding function such that N $ ψ B $ . All the states of the Boolean space eventually reach a state in the admissible region:

B

  simulates N . Let s y i ÝÑ g s I be a transition in the model of N . As ψ : B p Y Ñ L Y is surjective, there exist two Boolean states w, w I B p Y such that: ψpwq s and ψpw I q s I . We prove that we can select w I in the preimage of s I so that a transition w m ÝÑ f w I exists in the model of the Boolean network B. Firstly, let us characterize s I based on w. s I g i psq s ¡y i by definition of transition (Section 2);

y

  i zm . Hence, by definition of a transition, we have w m ÝÑ f w I , meaning that B simulates N .

Theorem 2 .

 2 Consider the Boolean network B xf, p Y , M 0 y and the multivalued network N xg i , Y, 1 y i y, related by the bisimulation B ψ N . Pick an M 0 -admissible mode M 2 p Y and consider the Boolean network B I xf, p Y , M y. We will show that B I bisimulates N , B I ψ N , by directly checking clauses (1) and (2) of the definition of bisimulation (Definition 1). Clause (1) (forward simulation): Take two Boolean states w, w I dom ψ such that w m ÝÑ f w I for some m M . We can then write the following deduction: w m ÝÑ f w I ùñ hm 0 M 0 , hw P dom ψ w m 0

  The two previous paragraphs show that the clauses of the definition of bisimulation (Definition 1) are satisfied for the Boolean network B I , running under mode M , and for the multivalued network N , meaning that B I ψ N . The associated function mapping the modalities of B I to those of N is the unique total function 2 p Y Ñ ty i u (i.e., the same as for the bisimulation B ψ N ).Proposition 2. By definition of a transition (Section 3.2) we have:dw, w I B p Y , dm M : w m ÝÑ w I ùñ dpw, w I q ¤ |m|,Therefore if the different coding of multivalued state complies to:

Proposition 4 .

 4 We denote: 0 m a Boolean state with 0 for all variables in m p Y . If a state is in the admissible region then it always reaches states in the admissible region, and only in the admissible region, by definition of bisimulation. If the Boolean state w B p Y is outside of the admissible region, w dom ψ, then it is not accounted for by the computation of admissibility of the guard condition, by definition of Ψ Ñ1 . Therefore we have: f m pwq 0 m , dm M . Thus, all the trajectories starting from w successively cancel (set to 0) the states of the variables of m M whenever the result of the cancellation leads to a state outside the admissible region; otherwise the proposition holds. As mM m p

  The set of parts of E is noted 2 E tE I | E I Eu. State. A state s is an application from variables Y to a domain of values D, i.e., s ty 1 Þ Ñ d 1 , . . . , y n Þ Ñ d n u and D Y pY Ñ Dq denotes the state space defined on variables Y . We define L Y as the state domain defined on the integral interval between 0 and L, i.e., L Y

  formally defines functional bisimulation, which depends on a partial function ψ : B X Ñ L Y decoding a Boolean state to an integer state. Definition 1. Given a Boolean network B xf, X, M X y and a multivalued network N xg, Y, M Y y, a pair of functions pψ, µq, with ψ : B X Ñ L Y a partial function and µ : M X Ñ M Y a total function, form a bisimulation if and only if the following properties hold:1. (forward simulation) for any two Boolean states w, w I dom ψ and m M X , w m ÝÑ f w I implies ψpwq µpmq ÝÑ g ψpw I q:

Table 1 :

 1 Example of codes for levels ranging from 0 to 3. The states correspond to the variable profiles pp y i1 , p

y i2 , p y i3 q. The links connect codes differing by 1, and the codes in bold correspond to Van Ham sequence.

  Hence the set of markers M p Definition 4 (Markers of sign). Let xg, Y y a multivalued network bisimulating a Boolean network xf, p Y y with xY, , σy and x p

		Y ,	, σ B y as their
	respective signed interaction graphs. M p
	of p Y defined by:	Y is a subset of Boolean variables

Y p

Table 3 :

 3 Summary of the properties in a conversion of the codings.

ÝÑ ¦ denotes the reflexive and transitive closure of ÝÑ.

The minterm of a state is a conjunction of the variables such that the unique interpretation satisfying it is the state itself, e.g., mintermpx 1 0, x 2 1q x 1 ^x2 .

variable to 1. This restricts the set of admissible encodings triggering the guard, outside of which the transition always shifts the support variable state to 0.

Let s y i ÝÑ s I be an integer unitary stepwise transition with s y i l and s I py i q l I such that |l ¡ l I | 1, and p y i be the support of y i ( p y i k p y i ), we denote by w ÝÑ w I the asynchronous Boolean transition bisimilar to s y i ÝÑ s I . Two cases where p y i,k 1 should be considered depending on the encoding of the levels: p y i,k is shifted from 0 to 1 during the transition (i.e., w p y i,k 0 and w I pp y i,k q 1), or p y i,k remains as 1 (i.e., w p y i,k 1 and w I pp y i,k q 1).

In both cases, we characterize for each Boolean variable the set of codes corresponding to the initial level l such that p y i k is either shifted to or remains at 1. The initial level l is determined from the target level l I by considering that it is either l I ¡1, l I or l I 1 by definition of an unitary stepwise transition.

We define the set of codes for the initial level such that p y i k is shifted from 0 to 1 during the transition (ψ is implicitly restricted to ψ : B p y i Ñ L y i ): Ψ 0Ñ1 pl I , p y i k q tw p y i dom ψ | h maxp0, l I ¡ 1q ¤ l ¤ minpl I 1, Lq : ψpw p y i q l w p y ik 0 ψpw p y i r p y ik Þ Ñ1s q l I u.

Similarly, we define the set of codes for which a shift from 1 to 0 occurs: Ψ 1Ñ0 pl I , p y i k q tw p y i dom ψ | h maxp0, l I ¡ 1q ¤ l ¤ minpl I 1, Lq :

Finally, we define the set of codes where p y i k is 1 in both l and l I :

The set of Boolean states coding for level l, always reaching state 1 and never a state 0 for p y i k in a transition to a code of level l I , is defined as:

Note that the set difference in the previous equation is not necessarily empty. Indeed, there may exist a pair of states w p y i and w I p y i , with ψpw p y i q l and ψpw I p y i q l I , such that w p y ik w I p y ik 1, but for which ψpw p y i r p y ik Þ Ñ0s q l I also holds. We need to exclude such states w p y i from Ψ Ñ1 pl I , p y i k q, because they 6 8 7 p

x p y 1 p y 2 p y 1 pp x p y 2 q p p y 1 2 p y 2 q p y 2 pp x 2 p y 1 q p2p x p y 1 q Bisimilar reflexive reduction. Under the asynchronous mode, some support variables may maintain their value inducing self-loops that are not bisimilar to any transition in the integer dynamics. In the running example, shifting y from 2 to 3 is bisimilar to p1, 0, 1q p y 2 ÝÑ p1, 1, 1q, which modifies the value of p y 2 . However, any of the Boolean variables may be updated in asynchronous dynamics leading to two self loops on p y 1 and p y 3 for maintaining the state of these variables at 1. Obviously, these self-loops are not bisimilar to the integer state transition since the variation of the integer state from 2 to 3 is carried out by one transition only. No alternatives preventing these additional self-loops in the Boolean network are possible since any one of the Boolean variables may be updated, but the state must not change for p y 1 and p y 3 . This situation explains why our method operates on reflexive reductions of the networks, effectively discarding these extra self-loops. Also notice that this transformation can only be performed if the integer level 0 is coded by the 0 Boolean profile, meaning that the behaviours of the multivalued and Boolean networks match when no guards are satisfied. The reflexive reduction of a network N is denoted N $ . p ùñ q Assume that Property (7) is met for the local-to-support mode M , i.e., dm M : m p y i ψpf m pwq w p y i zm q g i ¥ ψpwq.

Appendix

N simulates B. Let w m ÝÑ f w I , m M , be a transition in the model of B such that w, w I dom ψ. We define the transition ψpwq ÝÑ ψpw I q by application of ψ on w and w I . We have: ψpw I q ψpf m pwq w ¡m q by definition of a transition (Section 2);

ψpf m pwq w p y i zm q ψpw ¡ p y i q from (5) and ( 6); g i ¥ ψpwq ψpw ¡ p y i q from (7), true by hypothesis.

Set s ψpwq and s I ψpw I q. Then s ¡y i ψpw ¡ p y i q, because w ¡ p y i is the Boolean encoding of the rest of the state s ¡y i . We finally have:

ψpwq ÝÑ ψpw I q s ÝÑ g i psq s ¡y i s y i ÝÑ g i s I , which defines a transition of ÝÑ g i with the asynchronous mode 1 y i .

We deduce that the transition cannot be achieved between codes of the same integer, thus leading to:

As w I f m pwqw ¡m by definition of a transition, this statement is equivalent to (10), concluding that the equilibrium stability is preserved.

Lemma 2. let N be an asynchronous multivalued network bisimulating an asynchronous Boolean network B with: 1. w p y ik w I p y ik : in this case w w I leading to ψpwq ψpw I q since ψ is a function, thus satisfying ψpwq ¤ ψpw I q.

2. w p y ik w I p y ik : as only two values are possible, 0 or 1, we deduce that w I p y ik 1. Hence, w I can be defined as w I w r p

by hypothesis, we conclude from (12) that ψpwq ¤ ψpw r p y ik Þ Ñ1s q. This inequality is equivalent to ψpwq ¤ ψpw I q. dw, w I dom ψ :

Moreover, as ψ is a function defined on supports, we have:

In conclusion, the following statement holds:

Now we prove that Statement 4.1 is satisfied. The proof is given for positive interaction.

p ùñ q By definition (3), a positive interaction, p y i k p y j r is defined as:

From (L2.b), we can rewrite this statement as:

dw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i qψpw ¡ p y i q ψpw I ¡ p y i q ùñ f j,r pwq ¤ f j,r pw I q. Let v f j,r pwq w ¡x y j r and v I f j,r pw I q w I ¡x y j r , as f j,r pwq ¤ f j,r pw I q by hypothesis, we conclude that: ψpvq ¤ ψpv I q from (L2.a), thus leading to:

dw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i q ψpw ¡ p y i q ψpw I ¡ p y i q ùñ ψpf j,r pwq w ¡x y j r q ¤ ψpf j,r pw I q w I ¡x y j r q.

As N and B are bisimilar, Property (7) holds. By application of this property we have: ψpf j,r pwq w ¡x y j r q g j ¥ ψpwq and similarly for w I . Thus we deduce that:

dw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i q ψpw ¡ p y i q ψpw I ¡ p y i q ùñ g j ¥ ψpwq ¤ g j ¥ ψpw I q. Finally, as codom ψ L Y by definition, we can rewrite the previous statement as follows by setting, s ψpwq, s I ψpw I q : ds, s I L Y : s i ¤ s I i s ¡i s I ¡i ùñ g j psq ¤ g j ps I q, that defines the positive interaction on migs(N): y i y j .

p ðù q Assume that an interaction y i y j exists and there exist two Boolean variables p

y j with no positive interactions between these variables, i.e., p y i k σ p y j r ùñ σ $ . We give a proof for the case σ ¡; the proof for σ 0 is similar.

From definition of the interactions (3), we deduce that: hw, w I dom ψ : w p y ik ¤ w I p y ik w ¡ p y ik w I ¡ p y ik f j,r pwq ¡ f j,r pw I q.

From Property (L2.b), we can rewrite the previous statement as:

hw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i q ψpw ¡ p y i q ψpw I ¡ p y i q f j,r pwq ¡ f j,r pw I q. Let v f j,r pwq w ¡x y j r and v I f j,r pw I q w I ¡x y j r , as f j,r pwq ¡ f j,r pw I q by hypothesis, we conclude that: ψpvq ¡ ψpv I q from (L2.a), thus leading to:

dw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i q ψpw ¡ p y i q ψpw I ¡ p y i q ùñ ψpf j,r pwq w ¡x y j r q ¡ ψpf j,r pw I q w I ¡x y j r q.

As N and B are bisimilar, Property (7) holds. By application of this property we have: ψpf j,r pwq w ¡x y j r q g j ¥ ψpwq and similarly for w I . Thus we have:

hw, w I dom ψ : ψpw p y i q ¤ ψpw I p y i qψpw ¡ p y i q ψpw I ¡ p y i qg j ¥ψpwq ¡ g j ¥ψpw I q. As codom ψ L Y by definition, we can rewrite the previous statement as follows by setting, s ψpwq, s I ψpw I q : hs, s I L Y : s i ¤ s I i s ¡i s I ¡i g j psq ¡ g j ps I q, that contradicts the existence of a positive interaction y i y j , which is false by hypothesis.

The proof for negative interaction follows the same scheme. Thus, we conclude that Statement 4.1 is satisfied.

Corollary 1. If Property 7 holds then we deduce that B ψ N from Theorem 1. As B ψ N and M is an admissible mode we conclude from Theorem 2 that B I ψ N .

Theorem 3. We prove that (12) holds for a set of Boolean variables belonging to a support p y i .

Let p y i k be a Boolean variable of this set, two cases occur: either w p y ik 0, or w p y ik 1. For the latter, w is left untouched by substitution leading to ψpwq ψpw r p y ik Þ Ñ1s q since ψ is a function, thus fulfilling ( 12). Hence, we address the case when w p y ik 0 in the proofs.

Summing code. The following property holds when w p y ik 0:

thus, we have:

We conclude that: ψpwq ψpw r p y ik Þ Ñ1s .

Van Ham code. Van Ham code is a sub-code of the Summing code, thus complying to its results.

Gray code. Let p y i 1 be a Boolean variable carrying the most significant digit, we separate p y i 1 from the other variables in the definition of ψ: ψpwq

Hence, when w p y i1 0, we deduce that ψpw r p y i1 Þ Ñ1s q 2 | p y i |¡1 ψpwq, leading to ψpwq ψpw r p y i1 Þ Ñ1s q.

Thus we conclude that p Y is the set of markers for the Summing and Van Ham code, while tp y i 1 | y i Y u are the markers for the Gray code by application of Lemma 2.

Theorem 4. We first show that the computation of the Boolean function f defined by ( 15) is correct with respect to the integer function g and the asynchronous mode (A). Next (B), we examine the satisfaction of Property ( 7).

Finally we demonstrate the bisimulation of the reflexive reduction for both networks (C).

A) The construction of f is correct.

Let s y i ÝÑ s I be a multivalued transition, such that s I y i g i psq l I and s I y j s y j for all 1 ¤ j ¤ n, j $ i, by definition of the asynchronous dynamics.

We have: maxpl I ¡ 1, 0q ¤ s y i ¤ minpl I 1, L i q since the evolution is unitary stepwise. Two cases are considered qualifying whether s I y i $ 0 or s I y i 0. For each, we examine whether the target state of the support variable p y i k is 0 or 1. Let us consider the following cases: 1. s I y i $ 0: By definition of a multivalued network (1) C l Ipsq is necessary satisfied as l I s I y i $ 0. Let Rpy i q be the set of regulators of y i , we have: s Rpy i q C Rpy i q,l I. Hence, we deduce that w p w I p y ik 1: in this case w p y i belongs to Ψ Ñ1 pl I , p y i k q by definition, meaning that w admissible for the guard. Thus we have:

w I p y ik 0: in this case w p y i does not belong to Ψ Ñ1 pl I , p y i k q by definition meaning that w is not admissible for the guard. Thus we have: ÝÑ s I be a multivalued asynchronous transition such that s $ s I , then there exist w, w I B p Y such that ψpwq s, ψpw I q s I , by construction of f (A). Moreover, we have: ψpwq $ ψpw I q, leading to w $ w I , as ψ is a function. Thus, a Boolean support variable p y i k verifies that w p y ik $ w I p y ik , as g and f are neighbourhood preserving (9). In this case, we have: w I f i,k pwq w ¡ p y ik from (A). Thus, we have the following equalities:

s I = ψpw I q by definition of ψ;

= ψpf i,k pwq w ¡ p y ik q by construction of f (A);

= ψpf i,k w p y i z p y ik ¡ p y i q from (T1);

= ψpf i,k w p y i z p y ik w ¡ p y i q from (5); = ψpf i,k w p y i z p y ik qψpw ¡ p y i q by (5), (6); = ψpf i,k w p y i z p y ik q s ¡y i as s ψpwq. As s I g i psq s ¡y i by definition of a transition, we deduce by simplification of s ¡y i that: g i psq g i ¥ψpwq ψpf i,k w p y i z p y ik q, concluding that Property (7) holds.

C) Bisimulation between reflexive reductions. It follows from (B), that we can set that Property (7) holds whenever s y i $ g i psq. As the asynchronous mode is local-to-support, and we always have s y i ÝÑ s I ùñ s y i $ s I y i g i psq by reflexive reduction, we conclude by application of Theorem 1 that the reflexive reduction of the multivalued and Boolean networks are bisimilar with respect to ψ.