In Petri net systems, liveness is an important property capturing the idea of no transition (action) becoming non-fireable (unattainable). Additionally, in some situations it is particularly interesting to check if the net system is (marking) monotonically live, i.e., it remains live for any marking greater than the initial one. In this paper, we discuss structural conditions preserving liveness under arbitrary marking increase. It is proved that the deadlock trap property (DTP) is a necessary condition for liveness monotonicity of ordinary nets, and necessary and sufficient for some subclasses. We illustrate also how the result can be used to study liveness monotonicity for non-ordinary nets using a simulation preserving the firing language. Finally, we apply these conditions to several case studies of biomolecular networks.
Petri nets are a natural choice to represent biomolecular networks. Various types of Petri nets may be useful – qualitative, deterministically timed, stochastic, continuous or hybrid ones, depending on the available information and the kind of properties to be analysed. Accordingly, the integrative framework demonstrated by several case studies in [GHR+08], [HGD08], [HDG10] applies a family of related Petri net models, sharing structure, but differing in their kind of kinetic information.
A key notion of the promoted strategy of biomodel engineering is the level concept, which has been introduced in the Petri net framework in [GHL07]. Here, a token stands for a specific amount of mass, defined by the total mass divided by the number of levels. Thus, increasing the token number to represent a certain amount of mass means to increase the resolution of accuracy.
This procedure silently assumes some kind of behaviour preservation while the marking is increased (typically multiplied by a factor) to represent a finer granularity of the mass flowing through the network. However, as it is well-known in Petri net theory, liveness is not monotonic with respect to (w.r.t.) the initial marking for general Petri nets. Thus, there is no reason to generally assume that there is no significant change in the possible behaviour by marking increase. Contrary, under liveness monotonicity w.r.t. the initial marking we can expect continuization (fluidization) to be reasonable. However, only a particular kind of monotonicity seems to be needed for continuization: homothetic liveness, i.e., liveness preservation while multiplying the initial marking by k [RTS99], [SR02].
At structural level, (monotonic) liveness can be considered using transformation (reduction) rules [Ber86], [Sil85], [Mur89], [Sta90], the classical analysis for ordinary nets based on the Deadlock Trap Property (DTP) [Mur89], [Sta90], or the results of Rank Theorems, which are directly applicable to non-ordinary nets [TS96], [RTS98]. In this paper, we concentrate on the DTP, which will initially be used for ordinary net models, and later extended to non-ordinary ones.
This paper is organized as follows. We start off with recalling relevant notions and results of Petri net theory. Afterwards we introduce the considered subject by looking briefly at two examples, before turning to our main result yielding a necessary condition for monotonic liveness. We demonstrate the usefulness of our results for the analysis of biomolecular networks by a variety of case studies. We conclude with an outlook on open issues. 2
We assume basic knowledge of the standard notions of place/transition Petri nets, see e.g. [DHP+93], [HGD08], [DA10]. To be self-contained we recall the fundamental notions relevant for our paper.
A Petri net is a tuple N = hP, T, P re, P osti, and a Petri net system is a tuple Σ = hN , m0i, where – P and T are finite, non-empty, and disjoint sets. P is the set of places. T is the set of transitions. – P re, P ost ∈ N|P|×|T| are the pre- and post-matrices, where | · | is the cardinality of a set, i.e., its number of elements. For a place pi ∈ P and a transition tj ∈ T , P re(pi, tj ) is the weight of the arc connecting pi to tj (0 if there is no arc), while P ost(pi, tj ) is the weight of the arc connecting tj to pi. – m0 ∈ N|≥P0| gives the initial marking. – m(p) yields the number of tokens on place p in the marking m. A place p with m(p) = 0 is called empty (unmarked) in m, otherwise it is called marked (non-empty). A set of places is called empty if all its places are empty, otherwise marked. – The preset and postset of a node x ∈ P ∪ T are denoted by • x and x • .
They represent the input and output transitions of a place x, or the input and output places of a transition x. More specifically, if tj ∈ T , • tj = {pi ∈ P |P re(pi, tj ) > 0} and tj • = {pi ∈ P |P ost(pi, tj ) > 0}. Similarly, if pi ∈ P , • pi = {tj ∈ T |P ost(pi, tj ) > 0} and pi • = {tj ∈ T |P re(pi, tj ) > 0}. We extend both notions to a set of nodes X ⊆ P ∪ T and define the set of all prenodes •X := Sx∈X • x, and the set of all postnodes X • := Sx∈X x • . – A node x ∈ P ∪ T is called source node, if • x = ∅, and sink node if x • = ∅.
A boundary node is either a sink or a source node (but not both, because we assume a connected net).
Definition 2 (Petri net, behaviour). Let hN , m0i be a net system. – A transition t is enabled at marking m, written as m[ti, if
∀p ∈ •t : m(p) ≥ P re(p, t), else disabled. – A transition t, enabled in m, may fire (occur), leading to a new marking m0, written as m[tim0, with ∀p ∈ P : m0(p) = m(p) − P re(p, t) + P ost(p, t). – The set of all markings reachable from a marking m0, written as [m0i, is the smallest set such that m0 ∈ [m0i, m ∈ [m0i ∧ m[tim0 ⇒ m0 ∈ [m0i. – The reachability graph (RG) is a directed graph with [m0i as set of nodes, and the labelled arcs denote the reachability relation m[tim0.
Definition 3 (Behavioural properties). Let hN , m0i be a net system. – A place p is k-bounded (bounded for short) if there is a positive integer number k, serving as an upper bound for the number of tokens on this place in all reachable markings of the Petri net: ∃ k ∈ N0 : ∀m ∈ [m0i : m(p) ≤ k . – A Petri net system is k-bounded (bounded for short) if all its places are k-bounded. – A transition t is dead at marking m if it is not enabled in any marking m0 reachable from m: 6 ∃ m0 ∈ [mi : m0[ti. – A transition t is live if it is not dead in any marking reachable from m0. – A marking m is dead if there is no transition which is enabled in m. – A Petri net system is deadlock-free (weakly live) if there are no reachable dead markings.
– A Petri net system is live (strongly live) if each transition is live. Definition 4 (Net structures). Let N = hP, T, P re, P osti be a Petri net. N is – Homogeneous (HOM) if ∀p ∈ P : t, t0 ∈ p• ⇒ P re(p, t) = P re(p, t0); – Ordinary (ORD) if ∀p ∈ P and ∀t ∈ T , P re(p, t) ≤ 1 and P ost(p, t) ≤ 1; – Extended Simple (ES) (sometimes also called asymmetric choice) if it is
ORD and ∀ p, q ∈ P : p• ∩ q• = ∅ ∨ p• ⊆ q• ∨ q• ⊆ p•; – Extended Free Choice (EFC) if it is ORD and ∀ p, q ∈ P : p• ∩ q• = ∅ ∨ p• = q•.
Definition 5 (DTP). Let N = hP, T, P re, P osti be a Petri net. – A siphon (structural deadlock, co-trap) is a non-empty set of places D ⊆ P with • D ⊆ D • . – A trap is a non-empty set of places Q ⊆ P with Q • ⊆ • Q. – A minimal siphon (trap) is a siphon (trap) not including a siphon (trap) as a proper subset.
– A bad siphon is a siphon, which does not include a trap. – An empty siphon (trap) is a siphon (trap), not containing a token. – The Deadlock Trap Property (DTP) asks for every siphon to include an initially marked trap, i.e., marked at m0.
The DTP can be reformulated as: minimal siphons are not bad and the maximal traps included are initially marked.
Definition 6 (Semiflows). Let N = hP, T, P re, P osti be a net. – The token flow matrix (or incidence matrix if the net is pure, i.e., self-loop free) is a matrix C = P ost − P re. – A place vector is a vector y ∈ Z|P |; a transition vector is a vector x ∈ Z|T |. – A P-semiflow is a place vector y with y · C = 0, y ≥ 0, y 6= 0; a T-semiflow is a transition vector x with C · x = 0, x ≥ 0, x 6= 0. – The support of a semiflow x, written as supp(x), is the set of nodes corresponding to the non-zero entries of x. – A net is conservative if every place belongs to the support of a P-semiflow. – A net is consistent if every transition belongs to the support of a T-semiflow. – In a minimal semiflow x, supp (x) does not contain the support of any other semiflow z, i.e., 6 ∃ semiflow z : supp (z) ⊂ supp (x), and the greatest common divisor of x is 1. – A mono-T-semiflow net (MTS net) is a consistent and conservative net that has exactly one minimal T-semiflow.
For convenience, we give vectors (markings, semiflows) in a short-hand notation by enumerating only the non-zero entries. Finally, we recall some well-known related propositions (see for example [Mur89], [Sta90]), which might be useful for the reasoning we pursue in this paper.
Proposition 1 (Basics). 1. An empty siphon remains empty forever. A marked trap remains marked for ever. 2. If R and R0 are siphons (traps), then R ∪ R0 is also a siphon (trap). 3. A minimal siphon (trap) is a P-strongly-connected component, i.e., its places are strongly connected. 4. A deadlocked Petri net system has an empty siphon. 5. Each siphon of a live net system is initially marked. 6. If there is a bad siphon, the DTP does not hold. 7. A source place p establishes a bad siphon D = {p} on its own, and a sink place q a trap Q = { }
q . 8. If each transition has a pre-place, then P • = T , and if each transition has a post-place, then •P = T . Thus, in a net without boundary transitions, the whole set of places is a siphon as well as a trap (however, not necessarily minimal ones). 9. For a P-semiflow x it holds • supp(x) = supp(x) • . Thus, the support of a
P-semiflow is siphon and trap as well (however, generally not vice versa).
2. If N is ordinary and the DTP holds for m0, then hN , m0i is deadlock-free. 3. If N is ES and the DTP holds for m0, then hN , m0i is live. 4. Let N be an EFC net. hN , m0i is live iff the DTP holds.
We conclude this section with a proposition from [CCS91], which might be less known.
deadlock-freeness coincide in mono-T-semiflow net systems. 3
If a property holds for a Petri net N with the marking m0, and it also holds in N for any m ≥ m0, then it is said to be monotonic in the system hN , m0i. In this paper we are especially interested in monotonic liveness.
Let hN , m0i be a Petri net system. It is called monotonically live, if being live for m0, it remains live for any m ≥ m0.
We are looking for conditions, at best structural conditions, preserving liveness under arbitrary marking increase. To illustrate the problem, let’s consider a classical example [Sta90], [SR02].
Example 1. The net N in Figure 1 is ES, conservative, consistent, and covered by one T-semiflow. It is live for the given initial marking m1 = (2p1, p4). Adding a token to place p5 yields the initial marking m2 = (2p1, p4, p5) and the net system remains live for m2 ≥ m1. However, adding a token to p4 yields the initial marking m3 = (2p1, 2p4) and the net behaviour now contains finite firing sequences, i.e., it can run into a deadlock (dead state). Thus, the net system is not live for m3 ≥ m1. It is not monotonically live.
How to distinguish both cases? The net has two (minimal) bad siphons D1 = {p1, p2} and D2 = {p1, p3}. There is no chance to prevent these siphons from getting empty for arbitrary markings. D1 can potentially be emptied by firing t2 ∈ D1 • \ • D1, and D2 by firing t1 ∈ D2 • \ • D2. The latter case destroyed the liveness for m3 as it will equally occur for all initial markings allowing transition sequences containing one of the troublemakers, in this example t1 and t2, sufficiently often.
One lesson learnt from the previous example is, a net does not have to make use of the additional tokens. Thus, all behaviour (set of transition sequences), which is possible for m is still possible for m0, with m ≤ m0. However, new tokens may allow for additional system behaviour, which is actually well-known in Petri net theory, see Proposition 4. 2p1,2p4 t1 t2 p2,p3,2p4 t3 t1 p1,p2,2p5 p1,p3,2p4
p1,p2,p4,p5 p2,p3,p4,p5 p2,p3,2p4 2p2,2p5
Proposition 4. For any net N and two markings m and m0, with m ≤ m0, it holds LN (m) ⊆ LN (m0) [BRA83]; nevertheless, hN , mi may be live while hN , m0i not.
Example 1 is a mono-T-semiflow net, i.e., a net, where liveness and deadlockfreeness coincide (see Proposition 3). We look briefly at Example 2 to understand that this does not generally hold if there are several T-semiflows breathing life into the net.
Example 2. The net N in Figure 3 is a slight extension of Example 1. It is ES, conservative, consistent and covered by two T-semiflows: x1 = (t1, t2, t3), x2 = (t4, t5). It is live for the initial marking m1 = (2p1, p4). minimal deadlock, not containing a trap: D1={p1, p2}, D2={p1,p3}; t2 may clean D1, t1 may clean D2;
The net has the following minimal siphons D1 = {p1, p2}, D2 = {p1, p3, p6}, and D3 = {p4, p5}; the first two are bad siphons. With the initial marking mt2ra=nsi(t2ipo1ns,pt41,,2pt52),, Dt31 acraennobne-cloimvee. empty by firing twice t2 ∈ D1 • \ • D1, which destroys the liveness, without causing a dead state. The transitions t4, t5 are live, the others not. Thus, the net system is not live, but deadlock-free. NC ES
The loss of liveness is not necessarily monotonic itself; i.e., a net may be live for m1, non-live for a marking m2 with m2 ≥ m1, and live again for a marking m3 with m3 ≥ m2 (which works for all examples in this paper). Liveness may also be lost by marking multiples (homothetic markings). Examples 1 and 2 are homothetically live, Example 3 in Section 5 not. 4
Let us turn to liveness criteria suitable for our objective looking at ordinary nets first. Liveness criteria not relying on the marking obviously ensure monotonic liveness. Unfortunately, there are only a few.
First of all, there are some structural reduction rules, see, e.g., [Sil85], [Ber86], [Mur89], [SR99]. To give a sample, the following reduction rule is easy to accept: a source transition is live, and all its post-places are unbounded. The transition and its post-places can be deleted (for analysis purposes); the reduction can be iterated as many times it is applicable. Sometimes, this kind of reasoning allows to decide liveness (for examples, see Section 6).
Besides structural reduction we have the DTP, which in most cases does depend on the marking, but it is obviously monotonic w.r.t. the marking: if each siphon contains a marked trap at m, then – of course – it contains a marked trap at m0 ≥ m. Thus, the DTP-related conclusions on behavioural properties in Proposition 2 are monotonic as well:
Proposition 5.1 can be considered as a special case of the DTP. Then, there must be source transitions (see Proposition 1.8), and the net is not strongly connected and not bounded.
Lemma 1. Let be N an ordinary Petri net. If N is monotonically live, then there are no bad siphons.
Proof. We will prove its reverse – if there exist a bad siphon, then the net system is not monotonically live – by contradiction. Let PS be a bad siphon. Then there exist troublemaking transitions Θi ∈ PS • \ • PS . There must be such transitions, because otherwise PS • = • PS , and then the siphon PS would be a trap as well.
Since the net system is monotonically live, the marking of the places P \ PS can be increased in such a way that it will never restrict the firing of the transitions PS • , i.e., the transitions depending on the siphon. Therefore, we can consider the subnet restricted to PS in isolation.
We will show that the subsystem restricted to PS can be emptied eventually by increasing the marking, hence cannot be monotonically live. Obviously we can assume that PS is a minimal siphon. We consider two cases.
(1) The siphon has no forks (tj is a fork if |tj • | > 1). Based on the P-stronglyconectedness (see Proposition 1.3), there exists at least one path from each place p ∈ PS to one of the troublemakers Θi. Moving a token from p to • Θi does not increase the marking of any other place of PS not belonging to the considered path. Obviously, this path can contain joins (tj is a join if | • t| > 1), but we can add any tokens that are missing in the input places of the join. Firing the join, the marking of the places in the siphon is not increased. Using this process we can move the tokens from any p ∈ PS to some • Θi, and by firing Θi when it is enabled, PS can be emptied. Thus, the net system can not be monotonically live.
(2) On the contrary, let us assume that there exists at least one fork tj and let p1, p2 ∈ tj • be its output places. For the same reason as discussed in case (1), there exists a directed path from both places to one or several troublemakers. If all paths from p1 to any troublemaker Θi contain tj , then they form a trap. This is impossible because siphons are assumed to be bad. By symmetry, in the case in which the paths from p2 to troublemakers contain tj , there exists a trap as well.
Finally, let us assume that there exists a path from p1 to a troublemaker Θi and one path from p2 to a troublemakers Θk, none of them containing tj . On both paths the same kind of reasoning can be applied (in an iterative way if several forks appear). Therefore, the siphon can be emptied even if firing tj increases the tokens in PS .
Lemma 1 helps to preclude monotonic liveness for Examples 1 and 2 as well as for all other non-monotonically live examples we are aware of. Theorem 1. Let be N an ordinary Petri net. If hN , m0i is monotonically live, then the DTP holds.
Proof. The structural check of the DTP can have three possible outcomes. 1. If there are no siphons, then the DTP holds trivially and the net is monotonically live (see Proposition 5.1). 2. If there are bad siphons, then the DTP does not hold for any initial marking and the net is not monotonically live (see Lemma 1). 3. If each siphon includes a trap, then the maximal trap PT in every minimal siphon PS has to be initially marked to fulfill the DTP. Because we assume liveness of the net system, there has to be at least one token in each minimal siphon (see Proposition 1.5). Let us assume that a token is not in PT , but in a place p ∈ PS \ PT . If there exists at least one path without forks from p to a troublemaking transition Θi ∈ PS • \ • PS not containing any transition belonging to the trap, • PT , then p can be emptied using the same reasoning as used in the proof of Lemma 1, case (1). Therefore the net can not be live. If the path from p to a troublemaking transition Θi ∈ PS • \ • PS contains a fork, then the output places of the fork will be marked when p is emptied, and the paths from the output places of the forks to the output should be considered separately.
Finally, if all paths from p to the troublemaking transitions contain at least one transition • PT , then the trap PT is not maximal since PT together with all places belonging to the above mentioned paths (including all non-minimal ones) from p to transitions • PT are also a trap.
According to Theorem 1, the DTP establishes a necessary condition for monotonic liveness, which complements Proposition 5.3.
Corollary 1. A live ES net system is monotonically live iff the DTP holds.
Moreover, for those systems for which deadlock-freeness is equivalent to liveness, the DTP is a sufficient criteria for liveness monotonicity. This leads, for example, to the following theorem: Theorem 2. Let be N an ordinary mono-T-semiflow Petri net which for m0 fulfills the DTP. Then the system hN , mi is live for any m ≥ m0. Proof. It follows from Proposition 5.2 (DTP and deadlock-freeness monotonicity) and Proposition 3 (equivalence of liveness and deadlock freeness in mono-T-semiflow net systems).
Therefore, the DTP is a sufficient criterion for monotonic liveness of ordinary mono-T-semiflow net systems as well. In summary, while the DTP is in general neither necessary nor sufficient for liveness, it turns out to be the case to keep alive ordinary ES nets or ordinary mono-T-semiflow nets under any marking increase. 5
It is well-known that non-ordinary nets can be simulated under interleaving semantics by ordinary ones [Sil85] (see Figure 4 for an example). Let us look on the net structures we get by this simulation to learn how far the results for ordinary nets of Section 4 can be uplifted to non-ordinary nets. Example 3. We take a non-ordinary net from [SR02] and consider its simulation by an ordinary net, which we construct according to the general principle demonstrated in Figure 4.
The two net systems in Figure 5 are conservative, consistent, and live for the given initial marking. The ordinary net on the right hand side is not ES, and it a b a b p1 2 5 2 3 c d p1 c d has two minimal bad siphons {q1, p1, p1b, p1c}, {p2, p1, p1b, p1c}. Thus, according to Lemma 1, it is not monotonically live. Because our simulation preserves the projection of the firing language, in particular, preserves monotonicity of liveness. Thus, we conclude that the model on the left hand side is not monotonically live. Indeed, both nets are not live for any initial marking with an even number of tokens in p1, but live for infinitely many other markings greater than or equal to (1, 1).
As a consequence of firing simulation by the ordinary net systems of the non-ordinary ones (preserving always the markings of the places involved in the head of the tail and complement, here q1 and q1co), liveness monotonicity can be studied on the ordinary simulation.
p1c p1b p1 3 t1 p1 p2 2 t2 q1
q1co t1 p2 t2 We consider a variety of test cases of our benchmark repository to demonstrate the helpfulness of the DTP for biomolecular networks. The following list sketches some basic characteristics. The essential analysis results are summarized in Table 1. All models hold the DTP, they are consistent and (supposed to be) live. For non-ordinary nets, the DTP refers to its simulation by an ordinary one. 1. Apoptosis (size: 37 places, 45 transitions, 89 arcs) is a signal transduction network, which governs complex mechanisms to control and execute genetically programmed cell death in mammalian cells. Disturbances in the apoptotic processes may lead to various diseases. This essential part of normal physiology for most metazoan species is not really well understood; thus there exist many model versions. The validation by Petri net invariants of the model considered here is discussed in [HKW04], [HK04]. 2. RKIP (size: 11 places, 11 transitions, 14 arcs) models the core of the influence of the Raf-1 Kinase Inhibitor Protein (RKIP) on the Extracellular signal Regulated Kinase (ERK) signalling pathway. It is one of the standard examples used in the systems biology community. It has been introduced in [CSK+03]; the corresponding qualitative, stochastic, continuous Petri nets are scrutinized in [GH06], [HDG10]. 3. Biosensor (size: 6 places, 10 transitions, 21 arcs) is a gene expression network extended by metabolic activity. The model is a general template of a biosensor, which can be instantiated to be adapted to specic pollutants. It is considered as qualitative, stochastic, and continuous Petri net in [GHR+08] to demonstrate a model-driven design of a self-powering electrochemical biosensor. 4. Hypoxia (size: 14 places, 19 transitions, 56 arcs) is one of the wellstudied molecular pathways activated under hypoxia condition. It models the Hypoxia Induced Factor (HIF) pathway responsible for regulating oxygen-sensitive gene expression. The version considered here is discussed in [YWS+07]; the corresponding qualitative and continuous Petri nets are used in [HS10] to determine the core network. 5. Lac operon (size: 11 places, 17 transitions, 41 arcs) is a classical example of prokaryotic gene regulation. We re-use the simplified model discussed in [Wil06]. Its corresponding stochastic Petri net is considered in [HLGM09]. 6. G/PPP (size: 26 places, 32 transitions, 76 arcs) is a simplified model of the combined glycolysis (G) and pentose phosphate pathway (PPP) in erythrocytes (red blood cells). It belongs to the classical examples of biochemistry textbooks, see e.g. [BTS02], and thus of systems biology as well. The model was first discussed using Petri net technologies in [Red94]. Its validation by Petri net invariants is shown in [HK04], and a more exhaustive qualitative analysis in [KH08]. 7. MAPK (size: 22 places, 30 transitions, 90 arcs) models the signalling pathway of the mitogen-activated protein kinase cascade, published in [LBS00]. It is a three-stage double phosphorylation cascade; each phosphorylation/dephosphorylation step applies the mass action kinetics pattern. The corresponding qualitative, stochastic, and continuous Petri net are scrutinized in [GHL07], [HGD08]. 8. CC – Circadian clock (size: 14 places, 16 transitions, 58 arcs) refers to the central time signals of a roughly 24-hour cycle in living entities. Circadian rhythms are used by a wide range of organisms to anticipate daily changes in the environment. The model published in [BL00] demonstrates that circadian network can oscillate reliably in the presence of stochastic biomolecular noise and when cellular conditions are altered. It is also available as PRISM model on the PRISM website (http://www.prismmodelchecker.org). Its corresponding stochastic Petri net belongs to the benchmark suite used in [SH09]. We consider here a version with inhibitor arcs modelled by co-places. 9. Halo (size: 37 places, 38 transitions, 138 arcs) is a cellular signaling and regulation network, describing the phototaxis in the halobacterium salinarum [NMOG03]. It models the sophisticated survival strategy, which the halobacterium developed for harsh conditions (high temperature, high salt). A light sensing system and flagellar motor switching allows the cells to swim to those places of their habitat where the best light conditions are available. The model is the result of prolonged investigations by experimentally working scientists [Mar10]. 10. Pheromone (size: 42 places, 48 transitions, 119 arcs) is a signal transduction network of the well understood mating pheromone response pathway in Saccharomyces cerevisiae. The qualitative Petri net in [SHK06] extends a former ODE model [KK04]. The Petri net was validated by Petri net invariants and a partitioning of the transition set. 11. Potato (size: 17 places, 25 transitions, 78 arcs) describes the main carbon metabolism, the sucrose-to-starch breakdown in Solanum tuberosum (potato) tubers. The qualitative Petri net model was developed in cooperation with experimentally working scientists, experienced in ODE modelling. Its validation by Petri net invariants is discussed in [HK04], and a more detailed pathway exploration in [KJH05].
Contrary, the model of signal transduction events involved in the angiogenesis processes, which is discussed in [NMC+09] as a stochastic and continuous Petri net model (size: 39 places, 64 transitions, 185 arcs) is to a large extent covered by a (non-minimal) bad siphon. Thus, even if the net is live for a certain marking m, there is always a larger marking m0, which will allow to remove all tokens from the bad siphon. Consequently, an arbitrary marking increase will not preserve liveness. 7
The Petri nets for the case studies have been constructed using Snoopy [RMH10], a tool to design and animate or simulate hierarchical graphs, among them qualitative, stochastic and continuous Petri nets as used in the case studies in Section 6. Snoopy provides export to various analysis tools as well as import and export of the Systems Biology Markup Language (SBML).
The qualitative analyses have been made with the Petri net analysis tool Charlie [Fra09], complemented by the structural reduction rules supported by the Integrated Net Analyser INA [SR99]. 8
We have discussed the problem of monotonic liveness, with one of the motivations originating from bio-model engineering. We have presented a new result showing the necessity of the DTP for monotonic liveness.
Moreover, we immediately know – thanks to the well-known propositions of the DTP – that ordinary ES nets are monotonically iff the DTP holds. Furthermore, we know – because the DTP monotonically ensures deadlock freeness – that for any net class, in which liveness and deadlock freeness coincide, monotonic liveness is characterized by the DTP. We have shown one instance for this case: the mono-T-semiflow nets (MTS).
We have demonstrated the usefulness of our results by applying them to a variety of biomolecular networks.
One of the remaining open issues is: what are sufficient conditions for monotonic liveness for more general net structures? While none of our test cases is an MTS net, this line might be worth being explored more carefully, e.g. by looking at FRT nets (Freely Related T-Semiflows) [CS92] and extensions. Acknowledgements. This work has been partially supported by CICYT - FEDER grant DPI2006-15390 and by the European Community’s Seventh Framework Programme under project DISC (Grant Agreement n. INFSO-ICT224498). The work of M. Heiner was supported in part by the grant DPI200615390 for a stay with the Group of Discrete Event Systems Engineering (GISED); the main ideas of this paper have been conceived during this period. Ber86.
BL00.
BRA83.