A Petri net model is referred to as Boolean if the only possible markings are sets, i.e., places are marked or not without further quantification; moreover, also the enabling conditions and firing rule are based on this principle of set-based token arithmetic. Elementary Net systems are an example of a class of Boolean nets, and so are the recently introduced set-nets. In our investigation of the synthesis problem for set-nets, it would be useful to know how this new net model can be fitted into the general theory of net synthesis based on the generic concept of τ -nets. Here, we demonstrate how set-nets and the idea of Boolean operations on tokens provide an opportunity to classify a wide variety of Boolean nets that are amenable to region-based net synthesis.
Recently, in [
The new class of Petri nets, set-nets, provides a faithful computational model matching very closely that exhibited by reaction systems. The key difference between standard Petri nets like Place/Transition nets (PT-nets) and set-nets is that the former support multiset-based token arithmetic, whereas the latter support set-based (or Boolean) operations on tokens.
Thus, the computational intuition embedded in bio-processes has led to a new class of nets with yet to discover properties. On the other hand, an important motivation behind the wish to establish the link with net theory is to establish whether Petri net based concepts (such as causal processes) and methods (such as synthesis of nets from a specification of their behaviour) could be used to provide analytical tools for reaction systems.
The research presented in this paper originates with the synthesis problem
for set-nets. We show that the new class of nets can be treated within the
general theory of region-based net synthesis. More precisely, we show that
setnets are an instance of τ -nets [
The paper is organised as follows. First, we present the basics of set-nets
and other types of nets. Section 3 recalls the general setup of [
SET-nets, EN-systems, and PT-nets
In this section we present set-nets and relate them to elementary net systems
(en-systems) [
The main idea underlying set-nets is that there is no concept of token counting. Places are marked or not marked and arcs have no weights. In this way, set-nets resemble en-systems, a fundamental net model in the study of basic features of concurrent systems. However, the execution semantics of the two models differ significantly.
Both set-nets and en-systems have an (unweighted) net as their underlying structure. A net is a triple (P, T , F ) such that P and T are disjoint finite sets of places and transitions, respectively, and F ⊆ (T × P ) ∪ (P × T ) is the flow of the net. We use the standard dot-notation: for any place or transition x, we let •x = {y | (y, x) ∈ F } be its set of input elements and x• = {y | (x, y) ∈ F } its output elements. This extends in the usual way to sets of places and/or transitions. For en-systems, we have the additional structural assumption that the underlying net has no ‘self-loops’ i.e., •t ∩ t• = ∅ for all t ∈ T .
A marking of a set-net or en-system is a subset of places of their underlying net. A place belonging to a given marking is said to be marked. In diagrams, places are drawn as circles and transitions as rectangles. If (x, y) ∈ F , then (x, y) is an arc leading from node x to node y. Markings are indicated by drawing in each place belonging to a given marking, a small black dot (a ‘token’).
A set-net is a tuple N = (P, T, F, M0) such that (P, T, F ) is a net and M0 ⊆ P is its initial marking. A en-system is a tuple N = (P, T, F, M0) such that (P, T, F ) is a net without self-loops and M0 ⊆ P is its initial marking.
The dynamics of set-nets is defined as follows. Let N = (P, T, F, M0) be a set-net and let t ∈ T . Then t is enabled at a marking M if •t ⊆ M . In such a case, t can occur (fire), leading to the marking M = (M \ •t) ∪ t•. A subset U of T , a step, is enabled at M if •U ⊆ M . If U is enabled, it can occur, leading to M = (M \ •U ) ∪ U •.
Hence in a set-net, a step U is enabled whenever each of its input places belongs to the current marking, in other words, each of its elements is enabled. When U occurs, its input places lose their token, while all output places will be marked. If a place is both input and output for U , it is marked before and after the occurrence of U . Furthermore, output places of U that were marked before its occurrence will remain marked. It is also worthwhile to observe that there may be distinct transitions t, u ∈ U for which •t ∩ •u = ∅ or t• ∩ u• = ∅. This has no effect on their participation in the occurrence of U .
The dynamics of en-systems is defined in a similar way, except that the enabling conditions are crucially different. Let N = (P, T, F, M0) be an ensystem and let t ∈ T . Then t is enabled at a marking M if •t ⊆ M and t•∩M = ∅. If t is enabled at M , it can fire which results in the marking M = (M \ •t) ∪ t•. A step U of T is enabled at M if each t ∈ U is enabled at M and (•t ∪ t•) ∩ (•u ∩ u•) = ∅ for any two distinct transitions t, u ∈ U . Then U can occur leading to M = (M \ •U ) ∪ U •.
Hence, in an en-system, if a step U is enabled at marking M then each of its input places is marked and none of its output places is marked. Actually, a step can only ever be enabled if the input/output neighbourhood of the transitions in U do not overlap (i.e., if there is no structural conflict in U ).
In set-nets and en-systems markings are sets and tokens are manipulated using set-based rather than multiset-based arithmetic. We will refer to such Petri net models as being Boolean. In contrast to both set-nets and en-systems, and Boolean nets in general, Place/Transition nets (pt-nets) have a multiset-based arithmetic. 4
A (weighted ) pt-net is specified as a tuple N = (P, T , W, M0), where P and T are, as before, finite, disjoint sets of places and transitions; W : (P × T ) ∪ (T × P ) → N specifies the arcs of N by their weights; and M0 : P → N is the initial marking. In general, for pt-nets, markings are multisets, rather than sets. In diagrams, whenever W (x, y) ≥ 1 for some (x, y) ∈ (T × P ) ∪ (P × T ), then (x, y) is an arc from x to y; it is annotated with W (x, y) if this is 2 or more. Given a marking M of N and a place p ∈ P , we say that M (p) is the number of tokens in p. Note that the dot-notations are now multisets, indicating the multiplicity of each input/output element.
A transition t of N is enabled at a marking M of N , if •t ≤ M . If t is enabled at M , it can fire which leads to the new marking M = M − •t + t•. Thus M is obtained from M by deleting W (p, t) tokens from each place p and adding W (t, p) tokens to each place p. A step of a pt-net N is a multiset of transitions. Step U is enabled at a marking M of N if t∈T U (t) · •t ≤ M . Thus, in order for U to be enabled at M , for each place p, the number of tokens in p under M should at least be equal to the accumulated number of tokens needed as input to each of the transitions in U , respecting their multiplicities in U . If U is enabled at M , it may occur which leads to M = M − t∈T U (t) · •t + t∈T U (t) · t•. Thus the effect of executing U is the accumulated effect of executing each of its transitions (taking into account their multiplicities in U ). Note that there is no concept of structural conflict in the class of pt-nets: transitions may occur together in a step whenever a marking supplies enough tokens.
Inhibitor and activator arcs. To each of the above net models we can add inhibitor arcs and activator arcs connecting places to transitions, by adding relations Inh and Act to their specification. Given the set of places P and set of transitions T of a set-net, or en-system, or pt-net, Inh, Act ⊆ P × T define its set of inhibitor or activator arcs, respectively. For each transition t ∈ T , we denote ◦t = {p | (p, t) ∈ Inh} for the set of inhibitor places of t and t = {p | (p, t) ∈ Act } for its activator places. (Both notions are extended to sets of transitions, and to multisets, disregarding multiplicities.)
The intuition behind these context arcs is that in order for a transition to
be enabled at a marking, its activator places should be marked (have at least
one token) and its inhibitor places should not be marked (have no token). Thus
the dynamics of these extended net classes is adapted in the following way: a
step U is enabled at a marking when it is enabled in the underlying set-net,
or en-system, or pt-net, and U ⊆ M and ◦U ∩ M = ∅. When U is enabled
at M and it occurs, then the resulting marking is defined as before (here the
activator and inhibitor arcs have no effect). Note that this semantics is an a
priori semantics (see, e.g., [
Connections and connection monoids
Now we are ready to recall the general setup of [
Connection monoids describe the relation between a place and a step. A connection monoid (or conn-monoid) is a set S of connections with a commutative and associative binary composition operation ⊕, and a neutral element (identity) 0. We will use the same symbol S for a conn-monoid and for its underlying set of connections. Moreover, for each s ∈ S we let 0 s = 0 and n+1 s = ( n s) s for all n ∈ N.
Let S be a conn-monoid. Then, a net-type over S is a transition system τ = (Q, S, Δ) where Q is a set of states, and Δ : Q × S → Q is a partial function such that Δ(q, 0) = q, for all q ∈ Q. For every state q, the set enbld τ (q) = {s | Δ(q, s) is defined} consists of all connections from S that are enabled at q.
As an example let us consider the conn-monoid SPT = (N×N, ⊕, 0) with 0 = (0, 0) and point-wise arithmetic addition ⊕. Using this monoid, the connections between places and multisets of transitions in pt-nets can be expressed through the net-type τPT = (N, SPT , ΔPT ) over SPT , where ΔPT = {(n, (m, k)) → n − m + k | n ≥ m ≥ 0}. Intuitively, this states that a place containing n tokens enables steps which take no more than n tokens, and that the resulting number of tokens is n−m+k where m and k are the numbers of tokens taken and produced, respectively, by all occurrences of transitions in that step together. A fragment of τPT , interpreted as a labelled directed graph, is shown in Figure 1(d).
In general, each net-type τ = (Q, S, Δ) defines a class of nets, the so-called τ -nets. The net-type specifies through Q the values that can be assigned to places; through the connections in S the effect of combining connections; and through Δ, the enabling conditions and newly generated values.
A τ -net is a tuple N = (P, T, F, M0), where P and T are, respectively, disjoint finite sets of places and transitions, F : (P × T ) → S is a connection mapping, and M0 is the initial marking of N (in general, a marking is a mapping from P to Q). For a place p of N and a step U of transitions, we define the composite connection between U and p by F (p, U ) = t∈T ( U(t) (F (p, t)). Thus, if U is a set, then F (p, U ) = t∈U F (p, t) and F (p, ∅) = t∈∅ F (p, t) = 0.
A step U is (resource) enabled at a marking M if F (p, U ) ∈ enbld τ (M (p)) for every place p ∈ P . The firing of such a step produces the marking M such that M (p) = Δ(M (p), F (p, U )), for every place p ∈ P . The concurrent reachability graph CRG(N ) of N is formed by firing inductively from M0 all possible (resource) enabled steps of N . (1, 0) (0, 1) (1, 0) p (a) p 1 (c) (e) 0
2 p → 2 q → 0 b p → 0 q → 0 (g)
The net-type τPT defines τPT -nets. In order to view a pt-net as a τPT net, all one needs to do is to associate integers, representing the number of tokens, with each place, and set F (p, t) = (W (p, t), W (t, p)), for all places p and transitions t. The conn-monoid SPT together with the transition system τPT provides accurate information about the enabling and firing of steps U . Indeed, all one needs to do is to calculate F (p, U ) = (inwgt , outwgt) using the monoid operation of point-wise addition (for all input and output weights of all multiple occurrences of transitions in U ).
As an illustration, let us consider the pt-net depicted in Figure 1(a). This pt-net is represented by the τPT -net in Figure 1(c). Notice that, in particular, F (q, b) = (0, 0) means that q and b in Figure 1(a) are disconnected. Also the markings are represented (by indicating the number of tokens by an appropriate integer 0, 1, 2, etc.). Figure 1(b) gives the concurrent reachability graph. We furthermore obtain F (p, {a, c}) = (1, 0) ⊕ (0, 1) = (1, 1) and F (q, {a, c}) = (0, 1) ⊕ (1, 0) = (1, 1) which, together with ΔPT (1, (1, 1)) = 1, means that: (i) the net in Figure 1(a) enables the step {a, c} at the initial marking at which both p and q have one token; and (ii) its firing results in the same marking. On the other hand the step {c, c} is not enabled at the initial marking because F (q, {c, c}) = (1, 0) ⊕ (1, 0) = (2, 0) and (2, 0) is not enabled at 1. However, it is enabled at the marking M with M (q) = 2 and M (p) = 0 and then its firing results in the marking M with M (q) = 0 and M (p) = 2. Now focus in the concurrent reachability graph in Figure 1(b) on the local markings of the place p in combination with the connections that lead to changes of those local markings. We can do this by labelling each state with the corresponding marking of p, and each arc with the cumulative arc weight w.r.t. p of the step U labelling that arc i.e., F (p, U ). The result is shown in Figure 1(e). Repeating the same procedure for the place q, yields Figure 1(f ). Note that both graphs in Figure 1(e) and (f ) can also be seen in the graph of the net-type τPT , see Figure 1(d). 4
Connection monoids for en-systems and set-nets Starting from en-systems, we will now present a number of specific classes of Boolean nets defined on basis of their place-transition connections. In what follows we describe the structure of the connection monoids by a Cayley table displaying the outcome of all possible combinations of connections.
In en-systems, there are three basic connections between places and transitions: – F (p, t) = – F (p, t) = in p and t are disconnected (independent) there is an arc from p to t – F (p, t) = out there is an arc from t to p p p p t t t that p is empty after the occurrence of t. If p and t are not connected, t may always occur from the point of view of p and its occurrence has no effect on the marking of p. There is also an explicit reference to F (p, t) = in for the case that p is empty and one to F (p, t) = out when p is full. In these cases the marking of p prohibits the enabledness of t. In addition to the three standard types of connections, τEN has a special ‘blocking’ connection ⊥ which does not label any arc (is never enabled), hence ⊥ ∈/ enbld τEN (0) ∪ enbld τEN (1). The connection ⊥ is also used to capture structural conflict between transitions. As such it is a convenient device to capture precisely those steps which are not allowed, because of the internal conflicting relations between their transitions w.r.t. the place.
The conn-monoid SEN = ({ , out, in, ⊥}, ⊕EN , ). is defined through its Cayley table in Figure 2(b). Here out ⊕EN out = out ⊕EN in = in ⊕EN out = in⊕EN in = ⊥ corresponds directly to the requirement that the neighbourhoods of transitions in a step must be disjoint for it to be enabled to occur.
For example, if we have two transitions, t and u, both removing tokens from place p, t p u , thus both have p as an input place, then the connection of the step {t, u} w.r.t. p is calculated as F (p, {t, u}) = F (p, t) ⊕EN F (p, u) = in ⊕EN in = ⊥ implying that {t, u} can never occur together (on account of p).
0 in ⊥ out in (a)
1 out ⊥ ⊕EN in ⊥ out out in ⊥ ⊥ ⊥ ⊥ (b) out in ⊥ ⊥ ⊥ ⊥ ⊕EN out in out in
⊥ ⊥ ⊥ (c)
In all conn-monoids , will be the identity element and — if present — ⊥ is the absorbing element. The monoid SEN is the most restrictive monoid over , in, out, and ⊥, because its operation does not yield any non-⊥ results except when is involved. This is clearly seen in Figure 2(c) which depicts the non-trivial part of the Cayley table from Figure 2(b), while omitting the values implicitly due to commutativity. In what follows we will present conn-monoids using a minimal presentation of their Cayley table as in Figure 2(c).
A basis of a conn-monoid is any irreducible subset of its non-⊥ connections such that any other non-⊥ connection can be derived from it.
Proposition 1. { , in, out} is the only basis of SEN .
Proof. Follows directly from the table in Figure 2(c).
Now there are four basic connections between places and transitions: – F (p, t) = p and t are disconnected (independent) – F (p, t) = rem there is an arc from p to t – F (p, t) = ins there is an arc from t to p – F (p, t) = loop there is an arc from t to p, and from p to t p p p p rem ⊥ loop ins rem ins loop 1 ⊥ 0 out 1 ⊕SN ins ins
ins rem loop rem loop rem loop loop loop loop
(b) 0 ins ins 1
The simplified Cayley table of the conn-monoid SSN is shown in Figure 3(b). From the table we see, e.g., that if p is an output place of a transition t and input place to u, t p u , then the connection of the step {t, u} w.r.t. p is given by F (p, {t, u}) = F (p, t) ⊕SN F (p, u) = ins ⊕SN rem = loop and so, as far as p is concerned, {t, u} can occur if p contains a token; moreover, p will also have a token after the occurrence of {t, u}.
Another important property of the SSN monoid is the idempotence of its operation (the diagonal of the Cayley table of SSN ). This reflects one of the main features of set-nets, namely that since resources are not quantified, they can be used by many transitions with the same connectivity in tandem, as though they were just one such transition. Note furthermore, that since set-nets know no structural conflict, ⊥ is not introduced through ⊕SN . Consequently, ⊥ is not necessary in the case of τSN and SSN . Actually, also SPN did not need ⊥, as pt-nets know no structural conflicts either. However, if we consider the class of k-bounded pt-nets then the situation is rather different as the corresponding conn-monoid is defined as SBPT = ({⊥} ∪ Nk × Nk, +k, (0, 0)), where Nk = {0, 1, . . . , k}, ⊥ is the absorbing element, and, for all n, m, n , m ∈ Nk, (n, m) +k (n , m ) = (n + n , m + m ) if n + n ≤ k ∧ m + m ≤ k ⊥ otherwise .
Proposition 2. { , ins, rem} is the only basis of SSN .
Proof. Follows directly from the table in Figure 3(b).
This insight forms a formal justification of the way in which τSN -nets are drawn: direct dashed arrows are used for ins and rem, but loop as a ‘compound’ connection can be depicted by the ‘compound’ representation for ins and rem. Note that in the ⊥-less version of SSN , loop is the absorbing element, but this will change when we add inhibitor arcs. First however, we add inhibitor arcs to en-systems.
In comparison with en-systems, we now have one more connection to take into account: – F (p, t) = inh
there is an inhibitor arc from p to t
Figure 5 shows the net-type τENI , and the simplified Cayley table of the conn-monoid SENI = ({ , out, in, inh, ⊥}, ⊕ENI , ). From this we see that the monoid SENI captures an additional type of structural conflict: in ⊕ENI inh = inh ⊕ENI in = ⊥ . That out ⊕ENI inh = inh ⊕ENI out = out is a consequence of the a priori semantics.
Proposition 3. { , in, out, inh} is the only basis of SENI .
Proof. Follows directly from the table in Figure 5(b).
Again, we have to cater for one additional connection: – F (p, t) = inh there is an inhibitor arc from p to t p p t t inh 0 in ⊥ out in out inh ⊥ ⊕ENI out in inh out in inh ⊥ ⊥ (b)
⊥ inh 0 ins out
1 rem (a) rem ⊥ loop inh out ⊥ ins ins rem loop rem inh out ⊥ loop loop loop out out ⊥ inh ⊥ out (b) loop ⊥ out Proposition 4. { , ins, rem, inh} is the only basis of SSNI .
Proof. Follows directly from the table in Figure 6(b).
Like for SSNI , also the operation of SSNI is idempotent. Even stronger: Proposition 5. Let T = ∅ be a set of transitions and T = {F (p, t) | t ∈ T }. ⎧ ⎪⎪⎪⎪⎪ ins if T ⊆ {ins, } ⎪⎪ ⎪⎪⎪⎪⎪⎪ rem if T ⊆ {rem, } F (p, T ) = ⎨ inh if T ⊆ {inh, } if T = { } ∧ ins ∈ T ∧ rem ∈ T ∧ inh ∈ T ⎪⎪⎪⎪⎪⎪ out if T ⊆ {inh, ins, out, } ∧ (out ∈ T ∨ {inh, ins} ⊆ T) ⎪⎪⎪⎪⎪⎪⎩⎪ l⊥oop iofthTerw⊆is{ei.ns, rem, loop, } ∧ (loop ∈ T ∨ {rem, ins} ⊆ T) Proof. Follows directly from the table in Figure 6(b). The table shows that ⊕SNI is idempotent and that {ins, rem, inh, } is SSNI ’s basis.
The last connection we consider is: inh 0 out in (a) act 1 in act ⊥ out in inh act ⊥ ⊥ ⊥ ⊥
act ⊥ in (b)
In the simplified Cayley table of SENC , we see that inh ⊕ENC out = out and act ⊕ENC in = in. These pairs of connections reflect that while the transitions involved are enabled with respect to the given place (which should be empty for the inh and out connections, and marked for the act and in connections) they affect it in a different way. The connections that induce a state change (out and in) are ‘stronger’ , while the connections designated for testing (inh and act) are ‘weaker’. Proposition 6. { , out, in, inh, act} is the only basis of SENC . Proof. Follows directly from the table in Figure 7(b).
Again we add an activator connection: inh 0 ins out
1 rem rem ⊥ loop act inh out ⊥ ins
ins rem loop rem inh
out act loop rem inh ⊥ out (b) act ⊥ ⊥ out Proposition 7. { , ins, rem, inh, act} is the only basis of SSNI . Proof. Follows directly from the table in Figure 8(b).
There are 9 different patterns for the various connections: from 0 (unmarked) and from 1 (marked), either to 0 or to 1, or undefined; see Figure 9.
In each conn-monoid considered before, different connections had different topological patterns in the associated net-type. This changes now, as in τSNC both loop and act give rise to the same pattern. The effect of combining act and loop however is loop rather than act. This is because, according to the step semantics of set-nets, adding tokens happens after removing or testing. So, in this combination, loop as a connection that induces a change of the state is ‘stronger’ than act. Another interesting pair in the table is formed by act and rem. The effect of composing them is rem which differs from in due to the different underlying step semantics even though the arc pattern of rem in τSNC and that of in in τENC are the same.
Thus we arrive at the crucial point in our considerations where it becomes clear that the sophisticated (and sometimes surprising) nature of different connections necessarily involves algebraic properties in addition to topological ones. We now propose a general classification of all possible connections in Boolean τ nets. We take the general view that each connection defines enabling and effect, and has an associated strength (weak or strong).
Weak connections impose constraints only with respect to enabling, but unlike strong connections, they do not impose constraints on the state resulting from the transition firing. So, when combined with a transition with a stronger connection, it is the latter that dictates the final result. For example, loop is strong in SSN as it ‘finishes’ by adding a token in operational sense, as this is supported by the algebraic property of absorbtion. rem, on the other hand, is weak in SSN as with this connection the enabling conditions are important, but the state of the net place (connected in this way to some transition) after the transitions fired may be changed by another transition (removing tokens or testing precedes token insertion). This leads to 25 different connections ∂xy where x, y ∈ {w, s, w, s, n}. Here x refers to arrows outgoing from 0, and y refers to arrows outgoing from 1; w means a weak arrow, s a strong arrow, and n no arrow (non-enabledness); finally, (.) implies changing the state (from 0 to 1 or vice versa). In particular, we have the following encoding of the previously discussed connections: ⊥ ∂nn ∂ww in ∂ns out ∂sn ins ∂ss rem ∂nw loop ∂ns inh ∂wn act ∂nw The corresponding topological patterns are shown in Figure 10. inh out in 1 1 1 0 0 0 act ins rem 1 1 1 0 0 0 loop ⊥ 1 1 1
We will now formalise in a general way algebraic operations on the 25 connections. Almost all will be motivated by enabledness, and the idea of weak and strong. In this way, associativity will be automatic in most cases. Let ∂xy ⊕ ∂x y = ∂x x y y . where is a commutative operation given by: w w s s n w w s s n w w w s s s s s n s n n n n n
The intuition behind, for example, ∂ss is that the transition is always enabled but its execution keeps the marking in the place unchanged.
Proposition 8. Sconn = ({w, s, w, s, n}, , w) is a commutative monoid. Proof. We need to show that (a b) c = a (b c) for all a, b, c ∈ {w, s, w, s, n}. To start with, if n ∈ {a, b, c} then (a b) c = n = a (b c). Otherwise, we observe that the following hold: – If s ∈ {a, b, c} and s ∈/ {a, b, c} then (a – If s ∈ {a, b, c} and s ∈/ {a, b, c} then (a b) c = s = a b) c = s = a (b c).
(b c). ⊕ENC out in inh act ⊕ENC out in inh act out in inh act ⊥ ⊥ out ⊥ ⊥ ⊥ in inh ⊥ act out in inh act ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ inh ⊥ act
Theorem 1. Sbool = ({∂xy | x, y ∈ {w, s, w, s, n}}, ⊕, ∂ww) is a conn-monoid. Proof. Follows from Proposition 8 and ∂xy ⊕ ∂x y = ∂x x y y .
SSN , SSNI and SSNC are all sub-monoids of Sbool . The SSN sub-monoid is a special one; it is non-blocking as composing connections never yields ⊥.
We can now formally describe Boolean net models as those classes of nets that
are defined by a net type over (a submonoid of) Sbool . From [
Finally, we should point out that in order to arrive at this general classification of Boolean nets, we have had to make some (slightly arbitrary) assumptions when the intended operational meaning of a combination was not clear. In particular, w w has been defined in such a way as to give more priority to the change of state. This and perhaps other assumptions are not cast in stone. With differently motivated models in mind, one may freely modify them, study, appreciate the differences. Also, we decided to define s s as n because s and s are both strong and so ‘uncompromising’: one changes the state whereas the other insists on preserving the state. This contradiction cannot be reconciled. A posteriori vs. a priori execution semantics Interestingly, conn-monoids can distinguish between the ‘a priori’ semantics defined at the end of Section 2, and the ‘a posteriori’ execution semantics. In the setting of en-systems, ‘a posteriori’ is exactly the same as ‘a priori’ with one extra condition for an enabled set of transitions: •U ∩ U = U • ∩ ◦U = ∅. Figure 11 exhibits this difference. 6
Conclusions The reader might wonder why we included in our presentation pt-nets which are clearly non-Boolean nets. Apart from certain didactic motivations, we thought that pt-nets come with a ‘calculus of connections’ based on a simpler monoid of natural numbers. To our initial surprise, a similar effect can be achieved in our symbolic setting where the monoid of ∂xy connections is completely determined by a simpler monoid with the operation. This could, perhaps, suggest a general approach for constructing practical implementations of synthesis algorithms for set-nets.
Note that there are variations of Petri nets, such as Boolean Petri nets, where
adding a token to an already marked place does not add another token [