Synthesizing Petri nets from state-based models.
This paper presents a method to synthesize labeled Petri nets from state-based models. Although state-based models (such as Finite State Machines) are a powerful formalism to describe the behavior of sequential systems, they cannot explicitly express the notions of concurrency, causality and conflict. Petri nets can naturally capture these notions. The proposed method in based on deriving an Elementary Transition System (ETS) from a specification model. Previous work has shown that for any ETS there exists a Petri net with minimum transition count (one transition for each label) with a reachability graph isomorphic to the original ETS. This paper presents the first known approach to obtain an ETS from a non-elementary TS and derive a place-irredundant Petri net. Furthermore, by imposing constraints on the synthesis method, different classes of Petri nets can be derived from the same reachability graph (pure, free choice, unique choice). This method has been implemented and efficiently applied in different frameworks: Petri net composition, synthesis of Petri nets from asynchronous circuits, and resynthesis of Petri nets.
Introduction
In this paper we present a method which given a finite state model,
called Transition System (TS), synthesizes a safe Petri Net with
a reachability graph that is either isomorphic to the original TS
or isomorphic to a minimized version of the original TS. The
synthesized PN is always place-irredundant, i.e., it is not possible
to remove any place from the net without violating its behavior.
The synthesis method provides us with a technique for transforming
specifications. Given a model which can be mapped into
a TS, we can derive a PN which is equivalent to the initial model
of the process. In such a way we can create a tool which automatically
translates CSP, CCS, FSM, Burst Mode machines and other
models into labeled Petri Nets. Also, we can use this tool for
transformation of Petri Nets aimed at optimality under some criterion
(place count, transition count, number of places, PN graph
complexity, etc.) or for deriving a net belonging to a given class
(safe, Free-Choice, Unique-Choice, etc.) This opensup an avenue
for building interactive tools where a designer has the possibility
to play with a PN-like specification, performing equivalent transformations
of PNs, and/or transformations of other specifications
This work has been partly supported by the Ministry of Education of Spain
(CICYT TIC 95-0419).
y This work has been partly supported by the U.K. SERC GR/J78334.
z This work has been partly supported by the U.K. SERC GR/J72486 and by
MURST research project "VLSI architectures".
x This work has been partly supported by the U.K. SERC GR/J52327.
into PNs under different design constraints and optimization criteria

A basic intermediate object between a TS and a PN is a region
[11, 1, 3, 10]. "State" in safe Petri nets is distributed among places:
each state is a set of marked places, and each place is marked in a
set of states. A region in a Transition System is a set of states, such
that transitions in and out of it "mimic" the PN firing behavior
which un-marks predecessor places and marks successor places
of a transition. In this way, it is possible to identify regions with
places, and construct a PN which has exactly the same set of
labeled firing sequences as the TS.
The papers cited above provide the formal framework for our
contribution, but suffer from a series of problems:
ffl Their contribution was mainly theoretical, aimed at obtaining
a canonical representation of the PN, with as many places as
could be added without changing the behavior of the net. On
the other hand, we strive to minimize the number of places,
in order to make the final Petri Net more understandable by
the designer.
ffl They did not address the problem of merging and splitting
"equivalent" labels, i.e., those labels which model the same
event, but must be split in order to yield a valid Petri Net.
ffl They were limited to elementary TSs, which are quite re-
stricted, while we can handle the full class of TSs by means
of label splitting.
In this paper,we present an algorithm for generating acomplete
set of minimal regions (which are analogues to prime implicants
in Boolean minimization) and further for removing redundant regions
(which is similar to generating a prime irredundant cover
in Boolean minimization). We can either generate all irredundant
nets and take the minimum among them (an exact minimization
of places in PNs), or heuristically choose a minimal
place-irredundant net, if searching for a minimum one is too time
consuming.
The paper is organized as follows. Sections 2 and 3 formally
introduce Transition Systems, Petri nets and regions. Section 4
describes the synthesis algorithms in detail, and briefly outlines
extensions of the basic method to cope with a broader class of
specifications. Section 5 shows the experimental results obtained
by a practical application of the proposed methodology. Section 6
concludes the paper.
Models
2.1 Transition systems
A transition system (TS) is a quadruple [11]
where S is a finite non-empty set of states, E is a set of events,
is a transition relation, and sin is an initial state.
The elements of T are called the transitions of TS and will be
often denoted by s e
The reachability relation between states is the transitive closure
of the transition relation T . If there is a (possibly empty)
sequence of transitions oe between states s and s 0 , then this is denoted
by s oe
simply by s
We also write s e
and s oe
correspondingly. Note that each
state is reachable from itself. Furthermore, a TS must satisfy the
following four basic axioms:
A2. No multiple arcs between a pair of states:
A3. Every event has an occurrence: 8e
A4. Every state is reachable from the initial state:
A TS is called deterministic if for each state s and each label
a there can be at most one state s 0 such that s a
a TS is called non-deterministic.
(c)
p2p3 p1p3
p3
a
a b
c c
a b
a
c c
(a) (b)
p4 p3 p5
c
a

Figure

1: An example of Transition System (a), the corresponding
PN (b), its labeled RG (c)
A TS can be represented as an arc-labeled directed graph. A
simple example of a TS without cycles is shown in Figure 1,a.
2.2 Petri Nets
A Petri Net [12] is a quadruple
is a finite set of places, T is a finite set of transitions, F '
is the flow relation, and m 0 is the initial
marking. A marking is a function that assigns every place a
non-negative number of tokens. A transition t 2 T is enabled
at marking m 1 if all its input places are marked. An enabled
transition t may fire, producing a new marking m 2 with one less
token in each input place and one more token in each output place
expressing the same behavior as the TS from

Figure

1,a is shown in Figure 1,b.
The sets of input and output places of transition t are denoted
by fflt and tffl. The sets of input and output transitions of place p
are denoted by fflp and pffl. The set of all markings reachable in
N from the initial marking m 0 is called its Reachability Set. The
graph with vertices corresponding to markings of a PN and with
an arc (m in the graph if and only if called its
Reachability Graph (RG).
A labeled PN is a PN with a labeling function
which puts into correspondence every transition of the net with a
(called label) from the alphabet A. If no two transitions
have the same label (unique labeling), then each transition in the
net can be uniquely identified by its label. In such case we can
use the label as the name of the transition. In the RG of a labeled
PN, an arc between markings m 1 and m 2 is labeled by the label
(t) of the transition t, which fires between markings m 1 and m 2 .
Such RG is called a labeled RG.
One can easily check that the labeled RG Figure 1,c derived
for the PN from Figure 1,b is isomorphic to the TS (Figure 1,a).
A net is called safe if no more than one token can appear in a
place. Safe nets are especially widely used in many applications,
since they have simple verification algorithms [7] and simple
semantics. A net is called a pure net if (p; t) 2 F implies that
(t; p) 62 F , i.e., for each transition t the following condition is
net is called simple if no two transitions
have the same sets of input and output places (i.e.,
2.3 Equivalence
This paper presents an algorithm for transforming TSs into PNs.
The notion of equivalence in such transformation is based on isomorphism
of labeled graphs and variations of such isomorphism.
Two TSs
are isomorphic if there exist two bijections
and (s;
RG of a labeled PN can be always interpreted as a TS and therefore
the equivalence of a TS and the corresponding PN can be
viewed as an isomorphism of a TS and a RG of the corresponding
PN.
Often we will consider isomorphism of a TS and a minimized
version of another TS. For comparing two TSs with different
event counts a split-isomorphism is used. Two TSs
are split-isomorphic if there is another TS TS such
1. the underlying graphs of these three TSs are isomorphic, and
2. labels on arcs in TS 1 and TS 2 can be viewed as two different
enumerations of events from TS.
This enumeration corresponds to assigning instance numbers to
the events. For example, if in TS there are three arcs labeled with
the same event a, then in TS 1 one of these arcs can be labeled
with a 1 , and two others with a 2 , while in TS 2 all three arcs
can be assigned different instance numbers: a 1 ; a 2 ; a
procedure of assigning instance numbers to different occurrences
of labels in TS is called splitting.
All three notions of equivalence(isomorphism of TSs, isomorphism
with a minimized TS, and split-isomorphism) guarantee
that two equivalent TSs are bi-similar, which is a stronger condition
than language equivalence in general ([9]). This implies, for
example, that deadlock and liveness properties are preserved for
a PN generated from the TS.
Regions
be a subset of the states of a TS, S 1 ' S. If s 62 S 1 and
then we say that transition s a
and s 0 62 S 1 , then transition s a
Otherwise, transition
s a
does not cross S 1 . In particular, if s
then the transition is said to be internal to S 1 , and if s 62 S 1 and
then the transition is external to S 1 .
A subset of states, r, is a region if for each event e one of the
following conditions hold: all transitions labelled with e (1) exit
r, (2) enter r, or (3) do not cross r.
Let us consider the TS shown in Figure 1. The set of states
is a region, since all transitions labeled with a
and with b enter r 3 , and all transitions labeled with c exit r 3 . On the
other hand, fs is not a region since transition s 1
this set, while another transition also labeled with b, s 4
does not. Similar violations of the region conditions exist for two
transitions labeled with a. However, there are no violations for c
since both transitions labeled with c exit this set of states.
Each TS has two trivial regions: the set of all states, S, and
the empty set. Further on we will always consider only non-trivial
regions.
Let r and r 0 be regions of a TS. A region r 0 is said to be a
subregion of r iff r 0 ae r. A region r 0 is a minimal region iff r 0 is
not a subregion of any other region of the TS.
3.1 Properties of regions
The following propositions state a few important properties of
regions.
Property 3.1 If r and r 0 are two different regions such that r 0 is
a subregion of r, then r \Gamma r 0 is a region.
Property 3.2 A set of states r is a region, if and only if its coset
r is a region, where S is a set of all states of the TS.
Property 3.3 Every region can be represented as a union of disjoint
minimal regions.
Property 3.1 hasbeenmentioned in [3]. Property 3.2 was given
in [11]. Property 3.3 is a stronger refinement of the corresponding
property from [3], which shows that any region can be viewed as
a linear combination of the minimal regions. The proofs are given
in [4].
For each state s 2 S we define the set of non-trivial regions
containing s, denoted by Rs .
A region r is a pre-region of event e if there is a transition
labeled with e which exits r. A region r is a post-region of event
e if there is a transition labeled with e which enters r. The set
of all pre-regions and post-regions of e is denoted with ffi e and
e ffi respectively. By definition it follows that if r 2 ffi e, then all
transitions labeled with e enter r. Similarly, if r 2 e ffi , then all
transitions labeled with e exit r.
There are eight non-trivial regions in the TS from Figure 1:
g. All of these regions are
minimal. Pre-regions and post-regions are defined as follows:
a g.
3.2 Excitation and switching regions
While regions in a TS are related to places in the corresponding
PN, an excitation region [8] for event a is a maximal set of states
in which transition a is enabled. Therefore, excitation regions are
related to transitions of the PN.
A set of states S 1 is called a generalized excitation region (an
excitation region) for event a, denotedby GER(a) ( by ER j (a)),
if it is a maximal (a maximal connected) set of states such that
for every state s 2 S 1 there is a transition s a
!. The GER
for a is the union of all ERs for a. In the TS from Figure 1,a
there are two excitation regions for event a: ER 1
and ER 2 g. The corresponding GER for event a is
g.
Similarly to excitation regions, we define generalized switching
regions, GSR(a), and switching regions, SR j (a), as sets of
states reached immediately after the occurrenceof an event. In the
TS from Figure 1,a there are two switching regions for event a:
g. The corresponding GSR
for event a is g.
3.3 Elementary Transition Systems
3.3.1 Axioms for ETS
sin ) is called elementary [11] (ETS) if
it satisfies, in addition to (A1) - (A4), the following two axioms
about regions:
A5. State separation property:
A6. Forward closure property:
Axiom 5 implies that two different states must belong to different
sets of regions. Axiom 6 implies that if state s is included
in all pre-regions of event e, then e must be enabled in s. It is easy
to see that the TS shown in Figure 1 is elementary. The TS shown
in

Figure

2,a is a cyclic elementary TS, while Figure 2,b shows a
non-elementary TS. The forward closure property is violated for
events a and b. Let us consider event a. The only pre-region of
a is region fs g. Therefore ffi e ' Rs 7 , but there is no
transition labeled with a from s 7 .
a b
a
c
f
e
d
a b
a b
a b
a
c
GER(a)
preregion(a)
f
(a) (b)

Figure

2: Examples of elementary (a) and non-elementary (b)
TSs
It has been shown in [11] that if a TS is elementary, then a PN
with a reachability graph isomorphic to the TS can be constructed.
Proposition 3.1 Foreach elementaryTS there exists a safe, pure,
and simple PN such that:
1. each PN transition is labeled with an event of the TS;
2. no two transitions are labeled with the same event;
3. the RG of the PN is isomorphic to the TS.
The procedure given by [11, 3] to synthesize a Petri net from
an ETS is as follows:
ffl For each event a a transition labeled with a is generated in
the PN;
ffl For each (minimal) region r i a place p i is generated;
ffl Place p i contains a token in the initial marking m 0 iff the
corresponding region r i contains the initial state of the ETS
sin
ffl The flow relation is as follows: a 2 p i ffl iff r i is a pre-region
of a and a 2 fflp i iff r i is a post-region of a.
A PN which is synthesized from all regions is called a saturated
net. The net constructed from all minimal regions is called a
minimal saturated net. These nets are canonical, however, even
a minimal saturated net can be redundant. Places can still be
removed from it while still preserving the required isomorphism
between its RG and the ETS.By analogy with logic minimization,
a saturated net is like the set of all implicants for a Boolean
function, while a minimal saturated net is like the set of all prime
implicants. Our goal is to provide a method for constructing
an irredundant net with minimal regions, which is similar to an
irredundant cover of prime implicants.
Another important drawback of the described procedure is
that axioms 5 and 6 do not provide an efficient algorithm for
checking elementarity, since they require to derive all the regions
and also to check elementarity conditions for each individual state.
Our procedure is specifically aimed at deriving minimal regions
by using simplified elementarity checks, that admit an efficient
implementation.
3.4 Elementary and minimal Transition Systems
In this section we show the relationship between the elementar-
ity of a TS and its minimality. Let us first recall a few useful
definitions.
Two states s and s 0 of a TS are equivalent, s
sequence of transitions oe: s oe
if and only if s 0 oe
!. A TS is
called minimal if it contains no equivalent states. We say that the
confluence condition holds for states s and s 0 if there is a state s 00
which is reachable both from s and s 0 . Note that according to the
definition of reachability s 00 can coincide with s or s 0 .
The relation between minimality and elementarity of TS is
two-fold:
ffl If an elementary TS is not minimal, then for each pair of
equivalent states the confluence condition does not hold.
ffl If a TS is not minimal and there is a pair of equivalent states
for which the confluence condition is satisfied, then the TS
is not elementary.
a b
d
e
c
e
c d
e
f
p6 p7
a b
c d
e
f
a
a
a b
a
(a) (b) (c) (d) (e)

Figure

3: Minimality and elementarity
This relationship is illustrated by Figure 3. The TS in Figure
3,a is elementary. However, it is not minimal since s 4
and s 6 Obviously, the confluence condition for these two
pairs of states is not satisfied. A safe PN with an RG isomorphic
to this TS is shown in Figure 3,b. Places p 6 and p 7 corresponds to
the minimal regions fs 4 g. These places have no
output transitions (the corresponding regions do not serve as pre-
regions to any events). Therefore, these places can be removed
from the PN without changing its behavior.
The RG of the PN without p 6 and p 7 is isomorphic to the TS
shown in Figure 3,c, which is a minimized version of the initial

Figure

3,a).
Another TS example is given by Figure 3,d. This TS is not
minimal and also not elementary, since the state separation property
A6 is not satisfied for equivalent states s 1
g.
Note that the confluence conditions for equivalent states is sat-
isfied. The PN from Figure 3,e contains two places which corresponds
to regions r 1 and r 2 and two transitions labeled with a
and b. Its RG is isomorphic to a minimized version of the initial
non-elementary TS. After minimization, the TS from Figure 3
becomes elementary.
As indicated by the two examples in Figure 3 an implicit
minimization occurs (1) when regions which do not serve as pre-
regions are removed (Figure 3,a-c) or (2) when regions including
all equivalent states are generated (Figure 3,d,e).
3.5 Elementarity conditions
In this section we present conditions for elementarity which allow
for efficient checking. We first connect the notions of pre-regions
and post-regions with those of excitation and switching regions.
Property 3.4
1. A region r is a pre-region of event a iff
2. A region r is a post-region of event a iff
This property allows to construct regions which serve as pre-
regions starting with excitation regions. This allows for efficient
BDD-based implementation. The following property helps in
performing efficient PN synthesis.
1. If a TS is elementary, then the following three conditions are
(a) Excitation closure.
For each event a:
r2 ffi a
(b) Event effectiveness. For each event a: ffi a 6= ;;
(c) If the TS is not minimal, then for each pair of equivalent
states the confluence condition does not hold.
2. If a TS is minimal and the excitation closure and the event
effectiveness conditions are satisfied, then the TS is elementary

The proof is given in [4].
Let us consider again the non-elementary TS from Figure 2,b.
This TS is non-elementary, because the excitation closure condition
is violated for a and b. For example,
while the only pre-region of a, fs g, is a proper super-set
of ER(a). According to Proposition 3.2, if the generated PN
has an RG which is minimal, then only the excitation closure and
the event effectiveness conditions must be checked to verify the
elementarity of a TS. The event effectiveness condition is trivial
to check. The major new result, yielding our new synthesis
procedure, is the excitation closure condition.
4 Petri net synthesis
This section describes the algorithms for synthesis. The proof of
their correctness is given in [4].
4.1 Synthesis algorithms
The skeleton of the algorithm for synthesis of a PN is given by
the following pseudo-code.
begin
repeat /* Generation of pre-regions and label splitting */
split := false;
for each e 2 E do
split labels (e);
split := true;
end for
find irredundant cover;
map to PN;
The input of this algorithm is a TS. The output is a PN which
is equivalent to the initial TS. The function expand states
recursively generates all minimal regions which serve as pre-
regions for one event. These minimal regions are called minimal
pre-regions. Minimal regions which are not pre-regions are not
needed, since a PN with a minimized RG is generated (see section
3.4). The function find irredundant cover produces
an irredundant set of regions. From this set a place-irredundant
net is generated. This function is discussed in section 4.2. The
function split labels performs the splitting of labels if the
minimized version of the initial TS has been found to be non-
elementary. This function is discussed in section 4.3. Other
a b
c d
r3 r4 r5
a
c
d c
d
(b)
(a)

Figure

4: (a) Transition system. (b) Minimal saturated and place-
irredundant nets.
pre-region events pre-region events

Table

1: All minimal pre-regions of the transition system depicted
in

Figure

4,a
means of handling non-elementaryTSs, basedon using self-loops
and dummy transitions, are discussedin section 4.4. The function
map to PN is the final step for constructing a PN from the set of
regions, which has been described in section 3.3.
expand states (r,R)
begin
/* r is the set of states to be expanded */
collects all regions generated */
if r is a region then
return;
/* since any region expanded from r
would not be minimal */
find violating some region condition in
st set of states to legalize eg;
expand states (r 0 ,R);
/* For some conditions the set of states must be
expanded in two directions (see [4]) */
nd set of states to legalize eg;
expand states (r 0 ,R);
4.2 Irredundant regions
A set of regions R is called redundant if there is a region r 2 R
such that set of regions R \Gamma r still satisfies the excitation closure
(and therefore also the event effectiveness) condition. Otherwise
R is called irredundant. A region is said to be essential when it
cannot be removed from any set of regions without violating the
excitation closure of some event.
We will illustrate how an irredundant set of places can be
calculated by means of the example of Figure 4. Table 1 presents
all minimal pre-regions of the TS.
As a preliminary step, essential regions are calculated. A
region r is essential if there exists a state s 2 r and an event e
such that r 2 ffi e, s 62 GER(e) and for all r
we have s 2 r 0 (i.e., r is the only region that removes from the
GER(a)
a
a
c
c
a
a
c
c
b'
c c'
(a) (b)
b"

Figure

5: (a) Selection of a set of states to force the excitation
closure. (b) Forcing a set of states to be a region by means of
label splitting.
intersection of pre-regions a state in which e is not enabled). For
example, for event c we have
In this case, both r 0 and r 1 are essential, since none of them
can removed from ffi c without violating its excitation closure.
Similarly we can deduce that r 2 , r 4 and r 8 are also essential (r 2
and r 4 are essential for d, and r 8 for a; b). Thus we have four
non-essential regions: r 3 , r 5 , r 6 and r 7 .
Next, for each event with non-essential pre-regions (e and f
in the example), all minimal covers are implicitly generated. For
event e, we have two minimal covers: fr g.
For event f we also have two minimal covers: fr
g. Finding a minimum cost cover can be posed as
finding a minimum cost solution of a Boolean equation describing
the covering conditions (unate covering problem). To reduce
the complexity of the problem, essential regions are not
included. The equation corresponding to the example is as fol-
lows:
A cost must be assigned to each region, according to the objective
function to be minimized, which depends on the application.
For example, if we want to minimize the total number of places
and arcs (a heuristic measure of the "simplicity" of the PN), then
we can assign to each place p a cost of j ffl pj 1. If we
want to minimize only the number of places, then the cost of each
place is 1.
In our case, cost(r 3
and two minimum-cost covers exist: fr (the
former is shown in Figure 4,b, where the redundant places are
depicted by dotted lines). There is another possible solution
but it has non-minimum cost.
4.3 Label splitting
The set of minimal pre-regions of an event a is calculated by
gradually expanding GER(a) to obtain sets of states that do not
violate the "entry-exit" relationship. When the excitation closure
is not fulfilled (see proposition 3.2), i.e.
r2 ffi a
r 6= GER(a)
some events must be split to make the TS elementary. This
situation is illustrated in Figure 5,a. Event a has two minimal pre-
regions (r 1 and r 2 ) and their intersection is larger than GER(a).
The strategy to split events is as follows. During the expansion
of GER(a) towards the pre-regions of a, several sets of states are
explored. We focus our attention on those sets S such that
GER(a)
r2 ffi a
r
For each of these sets of states, the number of events that violate
the region conditions are calculated. Finally, the set that has the
least number of "bad" events is selected. If several sets have the
same number of "bad" events, the smallest one is selected.
The selected set of states is then forced to be a region. This is
done by splitting the labels of those events that do not fulfill the
region conditions. An example is depicted in Figure 5,b.
The strategy for splitting ensures that, with the new labeling,
there will be one pre-region smaller than the intersection of the
pre-regions with the former labeling. Next, pre-regions are re-
computed, and excitation closure is verified. If the closure test
fails, the procedure is executed again. This strategy converges
monotonically, and in the worse case splits all the labels, so that
each state of the TS trivially becomes a region. For practical ex-
amples, only one or two iterations are usually required to converge.
Obviously, the PN obtained after any splitting is split-isomorphic
to the initial TS.
4.4 Modifications of the basic synthesis method
The class of TSs and PNs that can be handled by our synthesis
procedure can be extended to include some non-elementary
TSs without using the label splitting technique. One powerful
extension, to non-pure nets, is concerned with allowing self-loop
regions to be involved in the excitation closure condition. A region
r is a self-loop region for an event e if it is not a pre-region and the
GER(a) is contained in r. Including a place corresponding to a
self-loop region into the set of input and output places does not
restrict the enabling conditions for an event unnecessarily. Yet it
allows to "trim" the intersection of pre-regions so that the given
event is not enabled in the states not included in its excitation
region. Non-pure nets appear to be very useful in practice, e.g.
modelling arbitration circuits in which one event asymmetrically
disables another event. More details on this extension and oth-
ers, such as inserting dummy events 1 and relaxing axiom A2 (PN
simplicity) can be found in [4].
Our basic synthesismethod (namely, excitation closure) can be
customized to satisfy the requirements of some classes of Petri nets
which can be useful in practice. In particular, it can produce free-choice
and unique-choice PNs, a class of nets allowing efficient
algorithms for their verification and circuit implementation. More
on that is also in [4].
Applications

Table

2 describes the results of the application of our algorithms to
the synthesis of Petri nets from transition systems obtained from
speed-independent circuits. This can be used to produce a user-readable
description of the functionality of a circuit, in the form
of a timing diagram-like labeled Petri net (a Signal Transition
Graph, STG). All CPU times are in seconds on a SUN SPARC
workstation. Z, S, P, T, F and M are the numbers of signals,
states, places, transitions, arcs and markings, respectively.
events whose firing producesno visible effect on the trace and bi-simulation
semantics [9].
circuit
unsafe 5 22 15 12 34 22 2.8
a 11 sen 19 85 44 38 93 85 31.2
dags55 19 130 43 38 342 130 121.9

Table

2: Synthesis of Petri nets from speed-independent circuits.
example initial PN final PN CPU
alloc-outbound 17 /
clock
future 31 / 28 / 62 / 36
intel div3 8 / 8 /
intel edge 28 / 36 / 72 / 28 15 /
isend 56 / 44 / 116 / 53 24 / 19 / 105 / 36 41.4
lin edac93 14 / 12 / 28
master-read 36 / 26 / 72 / 8932 33 / 26 / 66 / 8932 29.6
pe-rcv-ifc 43 / 38 / 96 / 46 26 / 21 / 118 / 37 33.9
pulse
vme read 41 /
vme write

Table

3: Petri net minimization.

Table

3 describes the results of the application of our algorithms
to the minimization of a given labeled Petri net. The same
notation is used for places, transitions, arcs and markings 2 .
The implemented tool, called petrify, is available at
http://www.ac.upc.es/"vlsi/petrify/petrify.html.
5.1 Counterflow pipeline processor: stage control circuit
As an application example, we used our method to derive a PN
specification and its circuit implementation for a stage control
circuit in a counterflow pipeline processor (for a complete description
of the architecture refer to [13]). Although some of the
steps were assisted by hand, our net synthesis approach played
a key methodological role. These steps are shown in Figure 6.
The original behavioral description of the stage control was taken
from C.E. Molnar in the form of a TS.
The two transformations performed at this level were (1) reducing
the model to asymmetric form, which would then allow to
(2) insert a (single) dummy transition (denoted by ffl). The legitimacy
of this reduction was verified by means of TS composition.
The latter proved that the reduced model preserved all the main
functionalities: the counterflow pipe remained deadlock-free and
guaranteed the propagation of instructions and results without
missing their synchronisation in those stages where they may
meet. The resulting TS is quasi-elementary in the sense that it
satisfies our extended conditions of elementarity. The subsequent
synthesis of the PN was performed using the techniques described
in this paper, including operating with self-loop regions. Region
r2 is a minimal region, which is a self-loop region for event PR.
On the other hand, the other self-loop region r6 (for event AR) is
2 the number of markings may differ when different markings of the original PN
correspond to equivalent states in the RG.
States:
I Instruction
e
F
R I
PR
AR AI
PI
PI
AI AR
AR PR
AI
PI
e
d2
AR?
PR=AR
g_i
sel
AI=PI
AI?
AI!
g_i
execution
AI - accept instruction
PI - pass instruction
EX execute instr.
Events:
F
PR
AI
AR
PI
AR
AI
PI PR
R I
Original
Model Transition System
"Quasi-elementary"
PI AR
AI PR
control exec
Petri Net Model
Circuit implementation

Figure

Counterflow pipeline example: from transition system
to circuit
not minimal; it is a union of minimal regions r2 and r4.
This example illustrates that the amount of search for a self-loop
region can be significant, hence the complexity of synthesizing
non-pure PNs can be much greater than for pure nets. In
the net model of the stage control circuit all events are uniquely
represented. It was then relatively straightforward to apply the
technique of [5], which systematically adds semaphores for conflict
places at the PN level. Finally, implementing semaphores by
mutual exclusion elements we can obtain a circuit implementation
(somewhat similar to a solution recently presentedby Ebergen [6])
shown in Figure 6.
5.2 Translation of high-level specifications
This section presents an example that illustrates how this method
can be useful for PN composition and translation from high-level
languages into Petri nets. The example is aimed at modeling
circuits obtained from TANGRAM descriptions (a CSP-like language
[2] for asynchronous circuit compilation).

Figure

7 depicts how the STG of the composition of two hand-shake
circuits (a sequencer and a parallelizer) is obtained. From
the STG of each handshake circuit, synchronization places between
events with the same labels are inserted (dashed places and
arcs). Each synchronization place receives arcs from the STG
modeling the circuit that "produces" the event (output channel)
and generates arcs towards the corresponding events at the input
channel. After composing several STGs, the internal events can
be removed (signals req 2 and ack 2). The elimination of internal
events is done at TS level, thus obtaining a TS with less states.
Finally, the STG for the whole circuit is derived by resynthesis.
We also performed an experiment by modeling a 3-token FIFO
ack_2
ack_4
ack_3
ack_3-
ack_4-
ack_2-
ack_2-
ack_0-
ack_1-
ack_1-
ack_3-
ack_4-
ack_0-
(a) (b)
(c)

Figure

7: (a) Handshakecircuits, (b) PN composition, (c) PN after
elimination of internal events and synthesis.
in TANGRAM that resulted in a system with 20 handshake cir-
cuits. By iteratively composing the STGs of neighbouring hand-shake
circuits and eliminating internal events (corresponding to
internal communication channels), we obtained an STG with 6
signals (3 channels), places, 23 transitions, 71 arcs and 50
markings (states).
6 Conclusions
Petri nets have been shown to be an appropriate formalism to
describe the behavior of systems with concurrency, causality and
conflicts between events. For this type of systems, the method
presented in this paper allows to transform different models (CSP,
CCS, FSMs, PNs) into a unique formalism for which synthesis,
analysis, composition and verification tools can be built. Synthesizing
Petri nets from state-based models is a task of reverse
engineering that abstracts the temporal dimension from a flat description
of the sequences of events produced by the system. The
synthesis method discovers the actual temporal relations among
the events. The symbiosis among the notions of ETS, region and
excitation region in the same method has been crucial to derive
efficient algorithms.
Generating a TS from a high-level description (such as CSP)
may suffer from the state explosion problem, thus making manipulations
at the TS level tedious or even impractical. For this
reason, we have chosen to use a symbolic (BDD-based) representation
of the TS. Even though BDDs do not always guarantee
compactness, we have observed that the regular interleaving of
events manifested by highly concurrent systems is well-captured
by symbolic representations.
This work has been mainly motivated by the activities carried
out by the authors in the area of asynchronous circuits. The wide
applicability of the method opens new possibilities to create a
framework with tools for synthesis, analysis and verification, in
which the designer can freely choose and mix different specification
formalisms.

Acknowledgements

We are grateful to Marta and Maciej Koutny, who directed us
towards the existing literature about regions, and to Marco A.
Pe"na for performing the experiments with TANGRAM.



--R

Polynomial algorithms for the synthesis of bounded nets.
Handshake circuits: an intermediary between communicating processes and VLSI.
On synchronic structure of transition systems.
Synthesizing Petri nets from state-based models
Designing asynchronous circuits from behavioural specifications with internal conflicts.
Personal communication.


A calculus of communication systems.
Petri nets and step transition systems.
Elementary transition systems.
Kommunikation mit Automaten.
The counterflow pipeline processor architecture.
--TR
Elementary transition systems
Concurrent hardware
The Counterflow Pipeline Processor Architecture

--CTR
Alex Kondratyev , Michael Kishinevsky , Alexander Taubin , Sergei Ten, Analysis of Petri Nets by Ordering Relations in Reduced Unfoldings, Formal Methods in System Design, v.12 n.1, p.5-38, Jan., 1998
Jordi Cortadella , Michael Kishinevsky , Alex Kondratyev , Luciano Lavagno , Alex Yakovlev, Methodology and tools for state encoding in asynchronous circuit synthesis, Proceedings of the 33rd annual conference on Design automation, p.63-66, June 03-07, 1996, Las Vegas, Nevada, United States
Pastor , J. Cortadella, Efficient encoding schemes for symbolic analysis of petri nets, Proceedings of the conference on Design, automation and test in Europe, p.790-795, February 23-26, 1998, Le Palais des Congrs de Paris, France
Alexandre Yakovlev, Designing Control Logic for Counterflow Pipeline Processor Using Petri Nets, Formal Methods in System Design, v.12 n.1, p.39-71, Jan., 1998
Michael Kishinevsky , Jordi Cortadella , Alex Kondratyev, Asynchronous interface specification, analysis and synthesis, Proceedings of the 35th annual conference on Design automation, p.2-7, June 15-19, 1998, San Francisco, California, United States
Marta Pietkiewicz-Koutny, Synthesising elementary net systems with inhibitor arcs from step transition systems, Fundamenta Informaticae, v.50 n.2, p.175-203, April 2002
asynchronous circuits;Finite State Machines;transition systems;synthesis;petri nets