Jetty Ma iej and Grzegorz Rozenberg Kleijn1, Koutny2,
bition/retardation. These intera tions determine the dynami pro esses taking Rea tion systems [2, 3, 710℄ are a formal framework for the investigation of an abstra t theory of these pro esses. pro esses arried out by bio hemi al rea tions in living ells. The entral idea The investigation of the omputational nature of bio hemi al rea tions is a repaper is to develop a faithful Petri net model of rea tion systems. The main between (a large number of) individual rea tions, and moreover these intera ausal pro esses) and methods (su h as synthesis of nets from a spe i ation of of this framework is that the fun tioning of a living ell is based on intera tions pla e in living ells, and rea tion systems form a formal framework for developing tribute to a omputational understanding of the fun tioning of the living ell. tions are regulated by two main me hanisms: fa ilitation/a eleration and inhisear h topi of Natural Computing. One of the goals of this resear h is to onmotivation behind this is to establish whether Petri net based on epts (su h as The model of rea tion systems is based on prin iples remarkably dierent from those underlying other existing models of omputation. The aim of this their behaviour) ould be used to provide analyti al tools for rea tion systems.
It is not the intention of this paper to provide dire t feedba k to the area of where is a rea tion system and is the initial state. (S, A, C0), (S, A) C0 ⊆ S any set of its entities. Then an initialised rea tion system is a triplet C A = Denition 2 (state of rea tion system). A state of a rea tion system is To des ribe possible transitions between these states, we need to say what is A rea tion system with ba kground set has exa tly potential states. S 2|S| meant by an o urren e of a rea tion or a set of rea tions. entities are either present or not, and produ ed or not, and rea tions an or annot o ur based only on the presen e or absen e of ertain entities. There not found in most other formal models of dynami systems. In parti ular, it is worthwhile to point expli itly to the ‘non- ounting’ features of rea tion systems: sense that the o urren e of one rea tion might imply that another rea tion whi h is also enabled at the urrent state, annot o ur. This, again, is a feature One may observe that there is no oni t between rea tions in the ‘ lassi ’ is no representation of multiple instan es of entities or multiple o urren es of parameters an be a ommodated. This is done through the use of measurement utive states of dynami pro esses.
Depending on the goal of a spe i resear h theme, many other onstru ts are resear h on rea tion systems. This resear h happens in the framework of reAlthough the goal of this paper is a faithful ‘translation’ of rea tion sysintrodu ed and studied (see, e.g., [2, 9, 10℄) they form various extensions of a tion systems where a rea tion system onstitutes the basi te hni al notion. where various numeri al parameters an be assigned to ( al ulated for) onse tems into Petri nets, we on lude this se tion with a number of omments about ations where one needs to assign quantitative parameters (time, on entrations, the basi notion of rea tion system. For example, there are many biologi al situtive model (they annot ‘ ount’), they an be extended so that su h quantitative . . . ) to states of a bio hemi al system. Although rea tion systems are a qualitafun tions whi h lead to rea tion systems with measurements (see [2, 3, 9, 10℄),
{x, z, qa, qb, qc} [{rx, rz , a, c}imax {y, z, z, qa, qb, qc} {x, x, x, z, qa, qb, qc} [{rx, rx, rx, rz , a, c}imax {y, z, z, qa, qb, qc} . is enabled at state We then an show that the translation is sound. νI (M ). a step of transitions of and returns a set of rea tions of as follows U NI (A) A, First, is a well-formed marking satisfying and if is a M0 ν(M0) = C0, M a well-formed marking, then for every rea tion is enabled at i a ∈ A, a M {a} well-formed marking and then is also well-formed. Se ond, if is M [U iM ′, M ′ M and It is then possible to show a number νI (M ) = S ∩ ||M || ϕI (U ) = A ∩ ||U ||. of results, where a marking of the ptia-net is alled well-formed if M NI (A) for every M (qa) = 1, a ∈ A. one takes a marking of and returns a state of and the other takes M NI (A) A,
M ′(q) = |M•q(∩q)U−| |q• ∩ U | + |•q ∩ U | iofth({eqr}wi×seU. ) ∩ Reset = ∅ nets. We assume familiarity with the basi on epts of high-level nets [13℄, in a reset ar depends on the urrent marking rather than on a xed input/output maximal parallelism. Reset ar s are a non-standard me hanism and, in parti uparti ular, ar ins riptions, a tivator and inhibitor ar s, and simple transition tended with reset ar s in addition to inhibitor and a tivator ar s as well as The two translations des ribed in the previous se tion use low-level pt-nets exguards. relation with its neighbourhood. To ope with this problem, we will now outline two translations from ontext-independent rea tion systems to high-level Petri lar, they do not as yet support a ausal pro ess semanti s. Moreover, the ee t of at the pri e of introdu ing non-standard reset ar s. one-to-one orresponden e between groups of exe uted rea tions and transitions, and One an then {x, z} [{r, a, c}imax {y, z, z} {x, x, x, z} [{r, a, c}imax {y, z, z}. one orresponden e between states and markings, one ould hange the rules for show that a ounterpart of Theorem 1 holds also in this ase, with dened as νII tokens. This would, of ourse, be a radi al departure from the standard Petri be des ribed in Se tion 5. inserting tokens into pla es, by basi ally applying an OR-treatment for arriving To remove the need to have reset ar s or, equivalently, to obtain a one-tobefore and As transition is always enabled, we now have a νI ϕII (U ) = U \ {r}. r net approa h, but one worth investigating. The resulting model of set-nets will {x 7→ {1}, y 7→ ∅, z 7→ {1}, w 7→ ∅, clk 7→ {1}}
[{an7→1, cn7→1, Xn7→1}imax {x 7→ {1}, y 7→ {2}, z 7→ {1, 2, 2}, w 7→ ∅, clk 7→ {2}}
[{bn7→2, cn7→2, Xn7→2}imax {x 7→ {1, 3}, y 7→ {2}, z 7→ {1, 2, 2, 3, 3}, w 7→ ∅, clk 7→ {3}} . x 1 y
NIII (A0) x ay 1 n
n + 1 n + 1 a clk a 1 y n n
n + 1 n + 1 ax hm ≥ ni b clk b 1 z n m 1
n + 1 c clk c 1 w n (b) NIV (A0) that OR-treatment of ausality has been onsidered in [20℄, but the underlying di ates the presen e of a resour e without any quanti ation. Hen e any number that resulted from loser investigations into the possibilities of an OR-treatment i ts over tokens in set-nets, unlike in en-systems or pt-nets. Similarly, pla es the presen e of a single entity. In this se tion, we introdu e set-nets, a model into Petri nets, a major and as far as we an tell insurmountable problem was In our attempts to obtain a dire t and elegant translation from rea tion systems the fa t that several transitions may insert tokens into a pla e representing output pla es (whether or not they were already marked). We will build up the features of on urrent systems, in luding oni t, ausality and independen e.
The main idea is that in a set-net there is no on ept of ounting. Pla es new model in two stages, introdu ing rst set-nets with only ow ar s.
However, their exe ution semanti s is dierent. In set-nets, a marked pla e inprin iple there was ompletely dierent from what we are going to propose. tary net systems (en-systems) [19℄ whi h is a fundamental model to study basi do not ount the tokens, and the ring of a transition simply marks ea h of its are marked or not marked and ar s have no weights. Set-nets resemble elemenof transitions that take input from this pla e an be red at the same time.
Moreover, ring a transition empties all its input pla es. Thus there are no onof arriving tokens representing the produ tion of entities by rea tions. Note of the rst one if all the pla es of the form ontain the same single token clk a (interleaving) ring rule and its behaviour losely simulates that of the net oband all the tokens in other pla es satisfy (Note that from ea h rea h- k, l l ≤ k. able marking of the se ond translation one an exe ute a sequen e of transitions The resulting high-level net is exe uted a ording to the standard sequential leading to a marking with this property.) tained by Method III, and so also the behaviour of the original rea tion system. itively, a marking of the se ond translation orresponds dire tly to a marking M We skip the full des ription of the relationship between these two nets. Intufor the rea tion system is a high-level net shown in Figure A0 NIV (A0) 2(b). there is more than one reason for blo king, an auxiliary transition is hosen There are two possible reasons why might be blo ked in y le One is the a n. presen e of a token in the pla e representing an inhibitor of and to he k for n a, lo al y le su iently high, e.g., transition in Figure The overall result ax 2(b). a han e to do so, and we he k this using extra a tivator ar s together with a for and to he k for this we use a transition with an inhibitor ar . However, we a, more ompli ated as it is a la k of token in the pla e representing a rea tant n s non-deterministi ally). this we use a transition with an a tivator ar , e.g., in Figure The other is ay 2(b). also need to ensure that all transitions whi h feed tokens to have already had s transition guard whi h evaluates to true if all su h feeding transitions have their r↓ a b q↓ of pla es an be used to provide a su ient ondition for deadlo k-freeness in ‘stru ture theory’ of pt-nets. To illustrate our point, let us onsider a basi setset of pla es is alled a trap if It an be easily seen Trap ⊆ Pl Trap• ⊆ •Trap. marked trap annot be ome empty by ring any transition. Both type of sets ar s), as it seems that one an attempt to develop for them a ounterpart of pla es is alled a siphon if Similarly, a non-empty Sphn ⊆ Pl •Sphn ⊆ Sphn •.
We have introdu ed rst basi set-nets (without inhibitor and a tivator pt-nets whi h was a major motivation behind the development of their stru ture net with at least one transition. A non-empty set of SN = (Pl , Tr , Flw , M0) that an empty siphon annot a quire a token by ring any transition, and a theory. As it turns out, the same an be done in ase of set-nets. 12 J.Kleijn, M.Koutny and G.Rozenberg 6 Rea tion systems and set-nets omponents are as in Denition 4, and the last one as in is enabled at a marking if and It is interesting to M •U ∪ U ⊆ M ◦U ∩ M = ∅. point) as su h an assumption is not ne essary. observe that an enabled step is always onsistent in the sense that U (•U ∪ U )∩ As before, given a transition representing a rea tion, the sets and t •t, ◦t t we do not require that these sets be non-empty in a set-net (at least at this The denitions and notations on erning the marking hange in are the SNIA with the notion of onsisten y introdu ed for rea tion systems.
Su h a property has a natural and dire t (as we will see) onne tion ◦U = ∅. orrespond to the rea tants, inhibitors and produ ts of this rea tion. However, same as for in Denition 7 with one ex eption, namely a set of transitions SN U hibitor ar s, as illustrated by the set-net in Figure representing the ontext- 4(a), and and a = ({r, q}, ∅, {r}) b = ({q}, {s}, {r, q}) c = ({q}, ∅, {s}) . independent initialised rea tion system where: A2 = ({r, q, s}, {a, b}, {q}), Modelling inhibition aspe ts of rea tions is rather straightforward using in
ν(M ) = M \({phI }∪{scpl | s ∈ S}) ϕ(U ) = U \({I}∪{s↓ | s ∈ S}∪{s↑ | s ∈ S}) . well blo king a transition whi h ould add a token to a marked pla e, are totally fundamental lass of en-systems [19℄ extended with inhibitor as well as a tivator to expe t that there were in the past net lasses with similar features. Indeed, the their treatment of oni ts between transitions a essing the same token, as Set-nets are so simple when it omes to their denition, that it is reasonable ar s [12, 17, 18℄ basi ally have the same stati stru ture as set-nets. However, r↓ a
r II q↓ b
q phII phI
s↓ c I s s↑
scpl Having said that, the semanti s onsidered in prior works known to us was tokens. Therefore, as far as we are aware, the model of set-nets is an original based on single transition rings, rather than (maximal) steps as is the ase dierent. The latter issue has been noted in the past, and the onstraint relaxed.
For example, there are variations of Petri nets, su h as Boolean Petri nets, where ontribution to the eld of Petri nets. for set-nets. Therefore, the previous models were not on erned with multiple we had to introdu e the non- oni t feature on the ow ar s onsuming the faithfully model rea tion systems. Furthermore, by aiming at a set-semanti s, inputs of tokens to a single pla e something whi h is essential if one wants to Also, behaviour of this kind was mentioned in [1℄ in the ontext of net synthesis. adding a token to an already marked pla e does not add another token [4, 5, 11℄. q0 We proposed modelling methods resulting both in low-level and high-level have essentially isomorphi state spa es. All these net models, however, exhibited of the evolutions of two orresponding models. In fa t, we established that they as the on epts of lo alities and lo ally maximal on urren y were derived from Petri net theory based on our experien es with rea tion systems in a similar way with the rea tion systems and their semanti s.
In this way we think we derived new interesting notions and ontributions to tion. For example, both high-level net models are intrinsi ally unbounded, and to the properties of the orresponding Petri nets and ausal pro esses. to dis over methods for he king properties of rea tion systems by relating them our previous investigation of a Petri net semanti s of membrane systems [15℄. nets. In all four ases, we established a lose orresponden e between the markon epts ould be deployed to analyse rea tion systems. In parti ular, we wanted de ien ies w.r.t. simpli ity and/or elegan e and/or tra tability of the translathe se ond of the low-level translations uses reset ar s. We therefore proposed ings of Petri nets and states of the original rea tion systems. The same was true The main initial motivation of our investigation was to see how Petri net based a new lass of Petri nets, alled set-nets, whi h we feel provide a strong mat h detailed arguments an be developed for any of the standard net lasses. An What we just presented is intuition rather than proof, however, we expe t that and and . In the standard Petri nets, in luding various M0[{u}iM M0 6= M the existing net lasses and therefore deserve to be re ognised as an original important onsequen e, however, is that set-nets are semanti ally dierent from hange the urrent marking. Similarly, and would imply M0[{t, u}iM M0[{u}iM extensions of pt-nets, and would imply that does not M0[{t, u}iM M0[{t}iM u as well as . Hen e we have: and M = M ′ = M ′′ M0 6= M M0[{t, u}iM M0[{t}iM that does not hange the urrent marking. Yet the simultaneous ring of and t t does hange the marking as . This would produ e a ontradi tion. u M0 6= M ontribution.