Compacting Petri nets behaviors means to develop a more succinct representation of all the possible executions of a net, still giving the capability to reason on properties fulfilled by the computations of the net. To do so suitable equivalences on alternative executions have to be engineered. We introduce a general notion of merging relation, covering the existing approaches to compact behaviors of nets, and we state some properties this kind of relations may satisfy. The classical merging relations, defined on unfoldings, do not in general satisfy the properties one may be interested in, and we propose how to add information to the executions in order to enforce some of these properties.
proposed, and these are based on giving precise criteria to identify conflicting
conditions in nets which are acyclic, i.e. the transitive and reflexive closure
of the flow relation is a partial order. In the case of merged process ([
We pursue this idea further, casting it in a general framework. We start choosing a representation of nets behaviors less constrained with respect to the usual notion of causal net on which unfoldings are based. Causal nets are acyclic safe nets where conditions may have at most one incoming arc. The uniqueness of incoming arcs, together with the safeness, guarantee that dependencies can be uniquely identified. Conflicts are deduced from conditions having more than one outgoing arcs (implying that various alternatives use that condition). We drop the assumption that each condition has at most one incoming arc, and we add the requirements that each transition in the net can be executed at most once (which is syntactically enforceable) and that restricting the net to all the transitions in a execution we obtain an acyclic net, where each condition has at most one incoming and one outgoing arc. Dependencies can be captured by looking at executions, and some conflicts may still be retrieved by looking at multiple outgoing arcs. We call these nets unravel nets. This notion covers the one of causal nets, as these are indeed unravel nets, whereas unravel nets may not be causal ones. Together with the notion of unravel net, we introduce a notion of conflict that it is not based on the syntax, like in causal nets, but on the semantics (the executions of the net), simply stipulating that two conditions are in conflict if they never appear together in an execution.
We can now put forward the general framework, that consists in taking a representation of the behaviors of a given net (in our case a labeled unravel net) and an equivalence relation defined on conditions of the chosen representation of the behaviors. The minimal requirement we put on this relation, which is called merging relation is that two different conditions in the relation should be equally labeled and in conflict.
N1 s c0
Consider the unravel net N1. Conditions c2 and c3 are in conflict and they have the same label p, and similarly for conditions c1 and c4 (here the label is q). In the net above the merging relation (denoted with ∼) stipulates that c2 ∼ c3, c1 ∼ c4, c6 ∼ c7 and c5 ∼ c8 (reflexive pairs omitted). The relation is identified pictorially with different colors. This is not the unique merging relation definable on this net, we could have chosen this other relation: c2 ∼ c7, c1 ∼ c4, c6 ∼ c3 and c5 ∼ c8 (again reflexive pairs omitted), and clearly the identity relation is a merging relation. Once that a merging relation is fixed, we can compact the behavior by merging the conditions in the same equivalence classes and identifying the equally labeled transitions having the same preset and postset. The result of this procedure is the net shown on the left. The condid q tion 0 is the equivalence class of c0, N2 b p e5 3 e7 c 1ca3n,ids2cth7theeaenqoduniefivnaolaeflnlycc1e4acnltadhsesc4oo,fne3c2ooffanccd56 e2 1 e4 d and c8. Transitions with the same labels are not identified as none of s 0 them has the same preset and postset.
We observe that the net obtained idene1 2 e3 c tifying equivalent conditions is not any a q longer an unravel net. In the execution e6 4 e8 d e1 followed by e3 and e4 the condition c p 1 is marked twice violating the requirement of being acyclic. The fact that e3 should be followed by e5 and not e4 has been lost in the compaction process.
The notion of merging relation covers the criteria used in merged and trellises lapisrboerscaepnsrcsoehcsin.esgIsnepsrtohtcheeescssa,tsaheretnoifcnegmapelroagibneetdleiasdnacdlawutarsyealsl- N3 b c7 q a p net where dependencies and conflicts can q c2 e2 p e4 c6 be found syntactically. The criterion to use c4 in case of merged processes is to consider two equally labeled conflicting conditions ci p c1 e1 c3 e3 c5 saanmd ecjtoakseneqoucicvuarlreenntcies, twhhaitchthiesydehfianveedthaes a p a p the number of conditions labeled as ci and cj that are encountered going back to the initial conditions, comprising ci and cj. In the net N1 the conditions c6 and the condition c7 have both one condition in their past which has the same label, namely c2 and c3 respectively, hence their token occurrence is 2. In the case of trellises processes the starting point is not only a branching processes, but here the nets considered are called multi-clocks nets. Multi-clocks nets are the product of various automata where only one place is initially marked and each reachable marking is such that each component has just one place marked. Due to this feature it is possible to identify, for each condition and each execution, the exact time in which the condition holds. The criterion is then the one of considering two equally labeled conflicting conditions ci and cj as equivalent is that they have the same time, which is defined as the number of conditions that are encountered going back to the initial conditions, comprising ci and cj. In the unravel net N3, the conditions c3 and c4 have the same label p and have the same distance from the initial conditions, and similarly c5 and c6. By identifying these conditions also the transitions e5 and e6 have to be identified, resulting in the net N4. 1 is the equivalence class containing c3 and c4, 2 the one with c5 and c6 and finally eˆ is the transition obtained fusing e3 and e4, has these two transitions have the same preset, the same postset and are equally labelled, thus they share the same future. b e2 e1 a c7 q 1 p a ˆ e 2 p
The criteria used to obtain merged and trellises processes may be generalized equipping the unravel net with a mapping that associate to each condition a unique number, which we can call the measure. Thus a merging relation is obtained making equivalent all the conditions having the same labels, the same measure and being pairwise conflicting.
N4 q c2 p c1
For the compaction process to be of real interest one would like to obtain a net which is possibly an unravel one, or that has strong relations with the unravel net we started with. In fact we devise two characteristic the compaction process may have. The first one is that to each execution in the compact net, at least an execution in the original one should correspond. The merging relation used to obtain N2 out of N1 does not fulfil this property, whereas it does the merging relation used to obtain N4 out of N3. When a merging relation fulfil this property we say that it is a reflecting merging relation. Clearly a reflecting merging relation always exists, as the identity relation is reflecting.
The property of being reflecting, adopting as the measure the token occurrence, can be enforced by enriching the starting unravel net. In the net N1 conditions are used both to represent dependencies and conflicts, and by fusing some of them the dependencies may be lost. Thus the idea is to add some conditions that captures the dependencies. These conditions are easily obtainable by considering the whole token count for each transition of net. The net N1 can be enriched as shown in the net N5, and the added conditions are labeled with the condition representing the dependency. N5
Among the added conditions, in this case, there is no equivalence, as all of
them have a different measure, the measure in this case being the one represented
by the whole token count for the transitions (details on how to determine this
measure can be found in [
Beside looking for reflecting merging relation, one could be interested in p d 3 c preserving some characteristic of the net. For instance, one may be inter- b 1 d q ested in preserving the fact that the resulting net is still an unravel one (and s the measure induced by the time in the compaction done with trellis processes has this characteristic) or being a 2 c p acyclic when restricted to a certain subset of conditions (again, when consider- q c 4 d ing the conditions belonging to an automata this is the case in trellis pro- p cesses). When properties fulfilled by the net we start with are preserved by the compaction process we say that the merging relation is preserving. The merging relation giving the net N6 preserves the property that, when only the added conditions are considered, the whole net is acyclic, and verification can be performed easily.