Abstract
Attractors of network dynamics represent the long-term behaviours of the modelled system. Their characterization is therefore crucial for understanding the response and differentiation capabilities of a dynamical system. In the scope of qualitative models of interaction networks, the computation of attractors reachable from a given state of the network faces combinatorial issues due to the state space explosion. In this paper, we present a new algorithm that exploits the concurrency between transitions of parallel acting components in order to reduce the search space. The algorithm relies on Petri net unfoldings that can be used to compute a compact representation of the dynamics. We illustrate the applicability of the algorithm with Petri net models of cell signalling and regulation networks, Boolean and multi-valued. The proposed approach aims at being complementary to existing methods for deriving the attractors of Boolean models, while being generic since it applies to any safe Petri net.
As we said before, an unfolding is an "acyclic" version of a net N . This notion of acyclicity is captured by Definition 4.
Definition 4 (Occurrence net). Let N = P, T, F, M 0 be a Petri net. We say that N is an occurrence net if it satisfies the following properties:
Introduction
Living cells embed multiple regulation processes that lead to several emerging phenotypes such as cell differentiation, division, or response to environmental stress or signals. A large part of these processes are often represented as interaction networks (e.g., signalling networks, gene regulation networks) that describe the influences between numerous entities (genes, RNA, proteins). The global dynamics of such networks can then be captured using qualitative modelling frameworks, such as Boolean or discrete networks, that describe the possible transitions between the qualitative states of the system.
In the landscape of dynamics of a network model, one can distinguish between the transient and long-run dynamics, the latter being our focus in this article. In qualitative models, the long-run dynamics are referred to as attractors, and are formally defined as the Bottom Strongly Connected Components (BSCCs) of the transition graph whose nodes are the global states of the network, and directed edges are the possible direct transitions between those states. One typically distinguishes between two kind of attractors: the fixed points, that are the states from which no further transition is possible; and the cyclic attractors, that are a set of states that can be visited infinitely often.
Characterizing the attractors of network dynamics is key for capturing the potential adaptation and differentiation processes the cell can undergo. In particular, one could verify, from a given state of the network, if the dynamics always converges toward a unique attractor or may diverge towards different attractors. The former indicates a deterministic long-term behaviour, whereas the latter suggests an indeterministic differentiation, potentially controlled by additional mechanisms not captured by the level of abstraction of the model.
In practice, given a qualitative model of a network, the computation of the attractors reachable from one (set of) states can become very expensive as the size of the network grows. The naive approach consisting in generating the transition graph and computing the BSSCs suffers from the combinatorial explosion of the state space (exponential with the number of components of the network) and the explosion of the number of transitions.
A part of the combinatorial explosion of dynamics is due to the concurrency between the asynchronous transitions: in a given state, several transitions may be independently fired, which results in numerous redundant interleavings of transitions in the concrete transition space.
Contribution. In this paper, we propose a new algorithm for characterizing all the attractors that are reachable from a given initial state in a qualitative model expressed with safe Petri nets [18] , a broad class of nets which encompasses asynchronous Boolean or multi-valued networks. Our algorithm exploits the unfoldings of safe Petri net in order to reduce the size of the state space to explore.
Petri net unfoldings [7, 8] aim at representing the state space rechable from an initial state by exploiting concurrency between transitions to prune redundant interleavings of these transitions. To our knowledge this is the first algorithm for computing all the reachable attractors which relies on unfolding structures. Our algorithm is applicable to any safe Petri net.
Whereas experiments on particular cases of biological networks show room for improvement, such a technique exploiting concurrency is foremost complementary to existing algorithms (which ignore this dynamical feature) and therefore appeals for designing combinations of techniques to make tractable the analysis of very large networks.
Related work. In the scope of Boolean networks, there has been numerous work to link the topology of the network (the interaction graph, giving signed relations between the components) with the fixed points -resulting in bounds or characterization of a subset of fixed points (e.g., [1, 23, 22] ); and with cyclic attractors, e.g., [24, 17] . While the full characterization of the fixed points of Boolean/multivalued networks can be quite efficient for large networks [20, 21, 12] , the complete characterization of cyclic attractors is still a challenging task due to the combinatoric explosition of the state space to explore. Symbolic representation of the state space using binary decision diagrams has been used by [11] to characterize attractors in synchronous and asynchronous Boolean networks. The relationships between attractors in synchronous and asynchronous settings has then been exploited in [3] to speed the exploration of all possible attractors in Boolean networks, as well as Boolean network reduction techniques in [29] . Approximate methods are also largely considered, such as in [30] , which selectively explore appropriate regions of the state space to derive a subset of cyclic attractors of the global network dynamics.
In this paper, we will focus on the use of unfolding to compute finite complete prefixes [14] of safe Petri nets. Finite complete prefixes contain all the reachable markings in a compact representation (the prefix is always smaller than the reachability graph). Unfoldings are very well suited to capture concurrent system dynamics, and can be efficient for reachability analysis [9] , for instance.
Outline. In Sect. 2, we give a formal definition of (safe) Petri nets and their attractors, and introduce a running example. In Sect. 3, we present the unfolding of safe Petri nets. In Sect. 4, we detail our new algorithm to derive the attractors of a safe Petri net using its unfolding. Finally, implementation and experimations on Petri net models of biological networks are discussed in Sect. 5.
Petri Nets and Attractors
A Petri net is a bipartite graph where nodes are either places or transitions. In this paper, we consider only safe Petri nets where a place is either active or inactive (in oppositon to general Petri nets where each place can receive an arbitrary number of tokens, safe Petri nets allow at most one token per place). The set of active places form the state, or marking, of the net. A transition is said enabled if all the places that are parents of the transition are active. In the semantics, the firing of a transition makes inactive the parent places and then makes active the children places, modifying the current marking of the net.
Formally, a (safe) Petri net is a tuple N = P, T, F, M 0 where P and T are sets of nodes (called places and transitions respectively), and F ⊆ (P × T ) ∪ (T × P ) is a flow relation (whose elements are called arcs). A subset M ⊆ P of the places is called a marking, and M 0 = {p 1 0 , . . . , p n 0 } is a distinguished initial marking. For any node x ∈ P ∪ T , we call pre-set of x the set The Petri nets we consider are said to be safe because we will assume that any reachable marking M is such that for any t ∈ T that can fire from M leading to M , the following property holds: From an initial marking of the net, one can recursively derive all possible transitions and reachable markings, resulting in the marking graph (Def. 1). The marking graph is always finite in the case of safe Petri nets. The attractors reachable from the initial marking of the net can then be fully characterized by the bottom strongly connected components of the marking graph (Def. 2).
Definition 1 (Marking graph). The marking graph of a Petri Net N is a directed graph G = (V, A) such that V is the set of all reachable markings (obtained from all the possible firing sequences) and
Definition 2 (Attractors).
An attractor is a bottom strongly connected component of G, that is a set A of markings such that either A = {M } and no transition is enabled from M ; or for every M ∈ A, the set of markings reachable from M is precisely A. 
Unfoldings
In this section, we explain the basics of Petri net unfoldings. A more extensive treatment of the theory explained here can be found, e.g., in [7] . Roughly speaking, the unfolding of a Petri net N is an "acyclic" Petri net U that has the same behaviours as N (modulo homomorphism). In general, U is an infinite net, but if N is safe, then it is possible [16] to compute a finite prefix P of U that is "complete" in the sense that every reachable marking of N has a reachable counterpart in P. Thus, P represents the set of reachable markings of N . Figure 2 shows a finite complete prefix of the unfolding of the Petri net of Figure 1 . In principle, the set of reachable markings can also be computed by constructing the marking graph (see Definition 1). However, the marking graph suffers from combinatorial explosion due to concurrency. For instance, suppose that N simply contains n independent concurrent actions. Then the only attractor of the net is reached by executing all n actions in any arbitrary order. However, the marking graph will uselessly explore all n! different schedules for executing them, and all 2 n intermediate markings.
Research into concurrent systems has produced a number of solutions to alleviate the problem of combinatorial explosion due to concurrency (and eventually other sources). In [16] , McMillan first proposed the use of finite unfolding prefixes. Esparza et al [8] later improved this solution. For instance, the unfolding of the previous example with n independent actions is simply of size O(n). With respect to the marking graph, an unfolding represents a time-space tradeoff: in general, a complete unfolding prefix P is much smaller than the marking graph of N , but the problem whether a marking M of N is reachable, given P, is NP-complete. However, this tradeoff is usually favourable [9] .
We now give some technical definitions to introduce unfoldings formally.
Definition 3 (Causality, conflict, concurrency). Let N = P, T, F, M 0 be a net and x, y ∈ P ∪ T two nodes of N . We say that x is a causal predecessor of y, noted x < y, if there exists a non-empty path of arcs from x to y. We note x ≤ y if x < y or x = y. If x ≤ y or y ≤ x, then x and y are said to be causally related.
x and y are in conflict, noted
We call x and y concurrent, noted x co y, if they are neither causally related nor in conflict.
1. The causality relation < is acyclic; 2. | • p| ≤ 1 for all places p, and M (p) = 1 iff | • p| = 0; 3. for every transition t, t # t does not hold, and {x | x ≤ t} is finite.
As is convention in the unfolding literature, we shall refer to the places of an occurrence net as conditions and to its transitions as events. Due to the structural constraints, the firing sequences of occurrence nets have special properties: if some condition c is marked during a run, then the token on c was either present initially or produced by one particular event (the single event in • c); moreover, once the token on c is consumed, it can never be replaced by another token, due to the acyclicity constraint on <.
for all e, e ∈ E with e < e, if e ∈ C then e ∈ C; and (ii) C is conflict-free, i.e. if e, e ∈ C, then ¬(e # e ). The cut of C, denoted Cut(C), is the set of conditions
Intuitively, a configuration is a set of events that can fire during a firing sequence of N , and its cut is the set of conditions marked after that firing sequence.
We can now define the notion of unfoldings. Let N = P, T, F, M 0 be a safe Petri net. The unfolding U = C, E, G, M 0 of N is an (infinite) occurrence net (equipped with a homomorphism h) such that the firing sequences and reachable markings of U are exactly the firing sequences and reachable markings of N (modulo h). U can be inductively constructed as follows:
1. The conditions C are a subset of (E ∪ {⊥}) × P . For a condition c = x, p , we will have x = ⊥ iff x ∈ M 0 ; otherwise x is the singleton event in • c. Moreover, h(c) = p. The initial marking M 0 contains exactly one condition ⊥, p for each initially marked place p of N . 2. The events of E are a subset of 2 C × T . More precisely, we have an event e = C , t for every set C ⊆ C such that c co c holds for all c, c ∈ C and { h(c) | c ∈ C } = • t. In this case, we add edges c, e for each c ∈ C (i.e. • e = C ), we set h(e) = t, and for each p ∈ t • , we add to C a condition c = e, p , connected by an edge e, c .
Intuitively, a condition x, p represents the possibility of putting a token onto place p through a particular firing sequence, while an event C , t represents a possibility of firing transition t in a particular context. Recall that a configuration C of U represents a possible firing sequence, whose resulting marking corresponds, due to the construction of U, to a reachable marking of N . This marking is defined as
Since U is infinite in general, we are interested in computing an initial portion of it (a prefix ) that completely characterizes the behaviour of N . It is known [16, 8] that the construction of such a complete prefix is indeed possible, and efficient tools [26, 13] exist for this purpose. The precise details of this construction are out of scope for this paper; for what follows it suffices to know that it essentially follows the construction of U outlined above but that certain events are flagged as cut-offs when they do not "contribute any new reachable markings" (these events are represented by dashed lines in Figure 2 ). The construction then does not continue "beyond" such a cut-off event.
Extracting attractors from unfoldings
Our method for finding the attractors of a Petri net N uses unfoldings in two steps: first to find a set of markings which intersects all the attractors, second to output the attractors as a set of finite complete prefixes.
Representation of attractors as finite complete prefixes
We first remark that finite complete prefixes of unfoldings are particularly well suited for the representation of attractors. In fact, every attractor A is a set of states which form a maximal strongly connected component of the marking graph of N . For every marking M in A, the attractor A is precisely the set of markings reachable from M . Hence it can be compactly represented as a finite complete prefix of the unfolding of the Petri net N initialized at M . Denote this prefix U M : the markings associated to the configurations of U M are precisely those of the attractor, moreover the prefix shows the dynamics of the net while in the attractor. Last, the size of U M (as number of non cut-off events) can be up to exponentially smaller (in case of highly concurrent behaviour) than the number of markings in the attractor, and never exceeds it. Figure 3 shows two attractors of the Petri net N of Figure 1 represented as finite complete prefixes. The one on the left, U {p4,p6} , represents the attractor containing the marking {p 4 , p 6 }. The one on the right represents the attractor made of the single marking {p 3 , p 2 } which is a deadlock.
Maximal configurations and attractors
We have shown the interest of prefixes for representing attractors. What we need is a way to find a set M of markings of the Petri net N which contains one marking per attractor. Given such M, the set {U M | M ∈ M} gives a complete characterization of the attractors of N . Now we show that the desired set M of markings can be obtained from the maximal configurations of a finite complete prefix of the unfolding of N . 
Definition 7 (maximal configuration). A configuration of a prefix is called
maximal if no other event of the prefix can be added to the configuration. Equivalently, the configuration is a deadlock of the prefix viewed as a Petri net.
For example, in the prefix shown on Figure 2 , the configuration corresponding to the firing sequence t 3 t 2 is not maximal because it can be extended, for instance by t 4 and the other event labeled t 3 , yielding this time a maximal configuration, which reaches the marking {p 4 , p 5 }. Notice that this marking is not a deadlock in the original Petri net, yet the configuration is maximal in the prefix. Property 1. Let N be a Petri net and U a finite complete prefix of its unfolding. For every attractor A of N , there exists a maximal configuration of U whose associated marking belongs to A.
Proof. Choose a marking M in A. Because U is complete, it has a configuration C whose associated marking is M . Now because U is finite, it has a maximal configuration C which extends C. The marking M associated to C is reachable from M , therefore it is also in A.
The prefix shown on Figure 2 has four maximal configurations. One is obtained after firing only t 1 ; its associated marking is the deadlock {p 3 , p 2 }. This marking is associated to another maximal configuration: the one obtained by firing t 3 and then t 2 t 1 concurrently with t 4 . The third maximal configurations is obtained by firing t 3 , then t 2 and t 4 concurrently, and then t 3 again; it reaches the marking {p 4 , p 5 }. Finally, one can fire t 3 , then t 2 t 1 and t 6 concurrently, and then t 5 ; it reaches the marking {p 4 , p 6 }.
One can check that every attractor has a marking in this set: the deadlock {p 3 , p 2 } is represented twice; the marking {p 4 , p 6 } represents the attractor {{p 3 , p 6 }, {p 1 , p 6 }, {p 4 , p 6 }}. The marking {p 4 , p 5 }, also associated to a maximal configuration of U, is not in an attractor.
Algorithm
Property 1 allows one to use finite complete prefixes to identify attractors: the set M max of markings corresponding to maximal configurations intersects all the attractors. But not all the markings in M max belong to an attractor. Also an attractor may contain several markings in M max .
In order to characterize the attractors of a safe Petri net N , we filter the set M max and keep only one marking per attractor. The idea is to remove iteratively the markings from which another marking of the set is reachable. The reachability checking is done again using unfoldings.
The algorithm is the following: Termination of the algorithm is straightforward. We prove that at every step of the algorithm, the set M intersects all the attractors. This property is preserved when we remove a marking M from M because, if M is in an attractor A, then the marking M ∈ M reachable from M is also in A. Notice also that, if M is not in an attractor, then at least one attractor A is reachable from M ; and because M ∩ A = ∅, M contains a marking M ∈ A which is reachable from M . This ensures that U M is added to the set of attractors iff M is in an attractor A and M ∩ A = {M }. 
Illustration on the running example

Implementation and Experimental Results
In order to test the applicability of our approach, we implemented a prototype of the algorithm described above using Mole [26] for computing the complete prefixes, and Minisat [6] for extracting the maximal configurations 1 .
We applied our algorithm for the identification of attractors of three qualitative models of biological networks taken from the literature. In all cases, we applied a transformation to safe Petri net (Appendix A) that consists in having one place for each qualitative level of each component of the network, and transitions corresponding to the asynchronous semantics, i.e., each transition will actually change the level of only one component. By construction, the places corresponding to the levels of each components are mutually exclusive. The initial marking may then correspond either to a single state of the qualitative model, or to several possible initial states by adding transitions that non-deterministically select the initial state for some components (Sect. A.2). In this latter encoding, the returned attractors are the attractors reachable from at least one of the possible initial state of the qualitative model. Tab. 1 sums up the results of computing the finite complete prefixes on the following regulatory networks: a multi-valued model of the lambda switch [27] , a Boolean model of he mammalian cell cycle [10] , a Boolean model of the ERBB receptor [25] , and a multi-valued model of fate determination in the Vulval Precursor Cells (VPC) in C. elegans [28] . For the ERBB model, two different initial settings have been tested: (1) when EGF is active; (2) when either EGF is active or inactive. For the other models, the initial state is the level 0 for all the components. The execution times are in the order of a fraction of a second for the two first models; in the order of a few seconds for ERBB; and around 15 minutes for the VPC model. For the latter, we note that starting from a different initial state leads to a combinatoric explosion of the complete prefix, showing room for improvement to handle large model in general. It is difficult to compare with other existing tools as most of them handle only Boolean networks and do not support the search from a given initial state. GINsim [19] also provides attractors computations from a given initial state, but it relies on explicit state transition graph computation, which is always larger than a complete prefix (Section 3). For instance on the VPC example, GINsim has been stopped after one hour.
We presented a new algorithm for computing all the attractors reachable from a given state in the general class of safe Petri nets, i.e., Petri nets having at most one token in each place. This class includes Boolean and multi-valued networks that are typically used to model the qualitative dynamics of biological networks.
Our approach relies on Petri net unfoldings that natively take into account the concurrency between transitions to produce a compact representation of the reachable states. Then, we use the notion of maximal configuration to derive, from the computed unfolding, a set of states that includes at least one state of each reachable attractor. This set of maximal configuration is then filtered to output exactly one state per reachable attractors. The identification of attractors is complete in the sense that all the attractors reachable from the supplied markings are detected, including fixed points and cyclic and complex attractors.
By the use of Petri unfoldings, we aim at reducing the complexity of exploring the full reachable space by inherently pruning redundant transitions due to some interleaving of concurrent transitions. We applied a prototype implementation of the algorithm to four biological networks ranging from four to eighty interacting components, either multi-valued or Boolean.
The unfolding technique mentioned in this paper is generic to any safe Petri net. This indicates several directions for improving its computation (including the extraction of maximal configurations) in the particular case of biological interaction networks, such as the use of contextual Petri nets [2] , merge processes [15] , unravelings [4] , and the use of the network topology and static analysis to prune non-necessary transitions and decompose the detection of attractors.
A Encoding asynchronous discrete networks with safe Petri Nets
A.1 Encoding with one initial state
In literature, Boolean and multi-valued networks modelling dynamics of biological influence networks are typically represented by functions associating for each component the levels towards which it evolves with respect to each possible level of its regulators. In order to encode their asynchronous dynamics in Petri nets, one need to have a transition-centered representation, instead of a function-centered. Informally, this can be achieved by having one place per possible level of each component (we note i u the place corresponding to the level u of component i), and listing the conditions for moving a token from i u to i u+1 and i u−1 . Such conditions can typically be built from the expression of the discrete functions of the network. Our encoding always results in safe Petri nets, which makes it different from [5] which relies on more advanced Petri nets semantics (multiple tokens on places and weighted arcs), A Discrete Network gathers a finite number of components i ∈ {1, · · · , n} having a discrete finite domain F i that we note F i = {0, · · · , l i }, l i being the maximum level for the component i. For each component i ∈ {1, · · · , n}, a map f i : F → F i is defined, where F = F 1 × · · · × F n , giving the next value of the component with respect to the global state of the network. Typically f i depends on a subset of components (its regulators) that we denote dep(f i ). In the case of Asynchronous Discrete Networks (ADN), a transition relation → ADN ⊆ F × F is defined such that x → ADN x if and only if there exists a unique i ∈ {1, · · · , n} such that x [i] = f i (x) and ∀j ∈ {1, · · · , n}, j = i, x [j] = x[j], i.e. one and only one component has been updated. This is formalised in Def. 8. Network (ADN) ). An ADN is defined by a couple (F, f 1 , . . . , f n ) where F = F 1 × · · · × F n , and ∀i ∈ {1, · · · , n}, f i : F → F i with F i = {0, · · · , l i }. Given two states x, x ∈ F, the transition relation → ADN is given by
Definition 8 (Asynchronous Discrete
x → ADN x ⇐⇒ ∃i ∈ {1, · · · , n}, f i (x) = x [i]∧∀j ∈ {1, · · · , n}, j = i, x[j] = x [j] , where x[i] is the i-th component of x. We note dep(f i ) ⊆ {1, · · · , n} the set of components on which the value of f i depends: ∀x, x ∈ F such that ∀j ∈ dep(f i ), x[j] = x [j], necessarily f i (x) = f i (x ).
In the scope of an ADN (F, f 1 , . . . , f n ), we use cond(x) to map a state to the set of literals for the presence of the components at the corresponding state, e.g., cond( 1, 0, 1 ) = {1 1 , 2 0 , where simplify is an operator to reduce the number of conditions, and cond(x)| dep(i) restricts the literals to those corresponding to components influencing i.
Finally, given an ADN (F, f 1 , . . . , f n ) and an initial state x 0 ∈ F, the corresponding safe Petri net is defined by (P, T, F, M 0 ) where P = {i u | i ∈ {1, · · · , n}, u ∈ {0, · · · , l i }}, M 0 = cond(x 0 ), and T and F are the smallest sets (w.r.t. inclusion) such that ∀i ∈ {1, · · · , n}, ∀u ∈ {0, · · · , l i }, ∀Φ ∈ conds i u+ ∪ conds i u− , ∃t ∈ T :
By construction, the Petri net is safe and for each i ∈ {1, · · · , n}, the places i 0 , · · · , i li are mutually exclusive.
A.2 Encoding with multiple initial states
When studying the dynamics of a qualitative network, one may want to consider several initial states, chosen nondeterministically. Using the construction depicted in the previous section, one can encode this indeterministic choice by adding a place, initially marked, per (independent) indeterministic choice, and a transition per corresponding (local) state. Fig. 4 illustrate this construction with either an indeterministic initial state for one component, or for several components. (right) indeterministic choice between the initial state of the couple 1 and 2: either 0, 0 or 1, 1 .

{'paper_id': '3520721', 'title': 'Characterization of Reachable Attractors Using Petri Net Unfoldings', 's2_url': 'https://api.semanticscholar.org/CorpusID:3520721', 'source': 'S2ORC'}