An Improvement of McMillan''s Unfolding Algorithm.
McMillan has recently proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique requires to construct a finite initial part of the unfolding of the net. McMillan's algorithm for this task may yield initial parts that are larger than necessary (exponentially larger in the worst case). We present a refinement of the algorithm which overcomes this problem.
Introduction
In a seminal paper [10], McMillan has proposed a new technique to avoid
the state explosion problem in the verification of systems modelled with
finite-state Petri nets. The technique is based on the concept of net un-
folding, a well known partial order semantics of Petri nets introduced in
[12], and later described in more detail in [4] under the name of branching
processes. The unfolding of a net is another net, usually infinite but with a
simpler structure. McMillan proposes an algorithm for the construction of
a finite initial part of the unfolding which contains full information about
the reachable states. We call an initial part satisfying this property (in fact
slightly stronger one) a finite complete prefix. He then shows how to use
these prefixes for deadlock detection.
The unfolding technique has been later applied to other verification prob-
lems. In [7, 8, 11] it is used to check relevant properties of speed independent
circuits. In [5], an unfolding-based model checking algorithm for a simple
branching time logic is proposed.
Although McMillan's algorithm is simple and elegant, it sometimes gen-
Institut f?r Informatik, Technische Universit?t M-unchen.
E-mail: fesparza-roemerg@informatik.tu-muenchen.de.
Partially supported by the Teilprojekt A3 SAM of the Sonderforschungsbereich 342
"Werkzeuge und Methoden f?r die Nutzung paralleler Rechnerarchitekturen".
y Institut f?r Mathematik, Universit?t Augsburg.
E-mail: Walter.Vogler@informatik.uni-augsburg.de.
J. Esparza, S. R-omer, W. Vogler
erates prefixes much larger than necessary. In some cases a minimal complete
prefix has O(n) in the size of the Petri net, while the algorithm generates
a prefix of size O(2 n ). In this paper we provide an algorithm which
generates a minimal complete prefix (in a certain sense to be defined). The
prefix is always smaller than or as large as the prefix generated with the
old algorithm.
The paper is organised as follows. Section 2 contains basic definitions
about Petri nets and branching processes. In Section 3 we show that McMil-
lan's algorithm is just an element of a whole family of algorithms for the
construction of finite complete prefixes. In Section 4 we select an element of
this family, and show that it generates minimal prefixes in a certain sense.
Finally, in Section 5 we present experimental results.
2 Basic Definitions
2.1 Petri Nets
A triple (S; T; F ) is a net if
The elements of S are called places, and the elements of T transitions.
Places and transitions are generically called nodes. We identify F with its
characteristic function on the set (S \Theta T ) [ (T \Theta S). The preset of a node
x, denoted by ffl x, is the set fy 1g. The postset of x,
denoted by x ffl , is the set fy 1g.
A marking of a net (S; T; F ) is a mapping S ! IN . We identify a marking
M with the multiset containing M (s) copies of s for every s 2 S. A 4-tuple
net system if (S; T; F ) is a net and M 0 is a marking of
(called the initial marking of \Sigma). A marking M enables a transition
is enabled at M , then it can occur, and its
occurrence leads to a new marking M 0 (denoted M t
defined by
for every place s. A sequence of transitions
is an occurrence sequence if there exist markings M 1 , M 2 ,
. , Mn such that
\Gamma! Mn
Mn is the marking reached by the occurrence of oe, also denoted by M 0
oe
\Gamma!
. M is a reachable marking if there exists an occurrence sequence oe such
that M 0
oe
\Gamma! M .
The reachability graph of a net system \Sigma is a labelled graph having the
set of reachable markings of \Sigma as nodes and the relations t
\Gamma! between
markings as edges.
marking M of a net is n-safe if M for every place s. We identify
1-safe markings with the set of places s such that M net system
\Sigma is n-safe if all its reachable markings are n-safe.
An Improvement of McMillan's Unfolding Algorithm 3
In this paper we consider only net systems satisfying the following two
additional properties:
ffl The number of places and transitions is finite.
Every transition of T has a nonempty preset and a nonempty postset.
2.2 Occurrence Nets
be a net and let x 1 , x 2 . The nodes x 1 and x 2 are in
conflict, denoted by x 1 #x 2 , if there exist distinct transitions t 1 ,
that belong to the reflexive and transitive
closure of F . In other words, x 1 and x 2 are in conflict if there exist two
paths leading to x 1 and x 2 which start at the same place and immediately
diverge (although later on they can converge again). For x 2 S [T , x is in
self-conflict if x#x.
An occurrence net is a net
ffl for every b 2 B, j ffl bj - 1,
ffl F is acyclic, i.e. the (irreflexive) transitive closure of F is a partial
order,
ffl N is finitely preceded, i.e., for every x the set of elements
belongs to the transitive closure of F is
finite, and
ffl no event e 2 E is in self-conflict.
The elements of B and E are called conditions and events, respectively.
Min(N ) denotes the set of minimal elements of B [ E with respect to the
transitive closure of F .
The (irreflexive) transitive closure of F is called the causal relation, and
denoted by !. The symbol - denotes the reflexive and transitive closure of
F . Given two nodes
nor x#y.
2.3 Branching Processes
Branching processes are "unfoldings" of net systems containing information
about both concurrency and conflicts. They were introduced by Engelfriet
in [4]. We quickly review the main definitions and results of [4].
be two nets. A homomorphism
from N 1 to N 2 1 is a mapping
In [4], homomorphisms are defined between net systems, instead of between nets,
but this is only a small technical difference without any severe consequence.
4 J. Esparza, S. R-omer, W. Vogler


1. A net system and two of its branching processes
ffl for every t 2 T 1 , the restriction of h to ffl t is a bijection between ffl t
(in
In other words, a homomorphism is a mapping that preserves the nature
of nodes and the environment of transitions.
A branching process of a net system
) is an occurrence net, and p is a homomorphism from
N 0 to N such that
(i) The restriction of p to Min(N 0 ) is a bijection between Min(N 0 ) and
(ii) for every e 1

Figure

1 shows a 1-safe net system (part (a)), and two of its branching
processes (parts (b) and (c)).
Two branching processes of a net system
are isomorphic if there is a bijective homomorphism h from N 1 to N 2 such
that Intuitively, two isomorphic branching processes differ only
in the names of conditions and events.
It is shown in [4] that a net system has a unique maximal branching
process up to isomorphism. We call it the unfolding of the system. The
unfolding of the 1-safe system of Figure 1 is infinite.
be two branching processes of a net
system. fi 0 is a prefix of fi if N 0 is a subnet of N satisfying
ffl if a condition belongs to N 0 , then its input event in N also belongs
to N 0 , and
An Improvement of McMillan's Unfolding Algorithm 5
ffl if an event belongs to N 0 , then its input and output conditions in N
also belong to N 0 .
and p 0 is the restriction of p to N 0 .
2.4 Configurations and Cuts
A configuration C of an occurrence net is a set of events satisfying the
following two conditions:
causally closed).
of conditions of an occurrence net is a co-set if its elements are
in co relation. A maximal co-set B 0 with respect to set inclusion
is called a cut.
Finite configurations and cuts are tightly related. Let C be a finite configuration
of a branching process p). Then the co-set Cut(C), defined
below, is a cut:
In particular, given a finite configuration C the set of places p(Cut(C)) is
a reachable marking, which we denote by Mark(C).
marking M of a system \Sigma is represented in a branching process fi of \Sigma
if fi contains a finite configuration C such that Mark . It is easy to
prove using results of [1, 4] that every marking represented in a branching
process is reachable, and that every reachable marking is represented in
the unfolding of the net system.
For 1-safe systems, we have the following result, which will be later used
in Section 4:
Proposition 2.1
be two nodes of a branching process of a 1-safe net
system. If x 1 co x 2 , then
Given a cut c of a branching process as the
is the unique subnet of N whose set of nodes is
is the restriction of p to the
nodes of N 0 . Further, we define p(c) as the multiset containing an instance
of the place p(b) for every b 2 c. The following result will also be used later:
Proposition 2.2
If fi is a branching process of (N; M 0 ) and c is a cut of fi, then * c is
a branching process of (N; p(c)). 2.2
6 J. Esparza, S. R-omer, W. Vogler
3 An Algorithm for the Construction of a
Complete Finite Prefix
3.1 Constructing the Unfolding
We give an algorithm for the construction of the unfolding of a net system.
First of all, let us describe a suitable data structure for the representation
of branching processes.
We implement a branching process of a net system \Sigma as a list
of nodes. A node is either a condition or an event. A condition is a pair
(s; e), where s is a place of \Sigma and e the input event. An event is a pair (t; B),
where t is a transition of \Sigma, and B is the set of input conditions. Notice
that the flow relation and the labelling function of a branching process are
already encoded in its list of nodes. How to express the notions of causal
relation, configuration or cut in terms of this data structure is left to the
reader.
The algorithm for the construction of the unfolding starts with the
branching process having the conditions corresponding to the initial marking
of \Sigma and no events. Events are added one at a time together with their
output conditions.
We need the notion of "events that can be added to a given branching
process".
Definition 3.1
be a branching process of a net system \Sigma. The
possible extensions of fi are the pairs (t; B), where B is a co-set of
conditions of fi and t is a transition of \Sigma such that
t, and
ffl fi contains no event e satisfying
PE (fi) denotes the set of possible extensions of fi. 3.1
Procedure 3.2 The unfolding algorithm
input: A net system
output: The unfolding Unf of \Sigma.
begin
pe := PE (Unf );
while pe 6= ; do
append to Unf an event of pe and a
condition (s; e) for every output place s of t;
pe := PE (Unf )
endwhile
An Improvement of McMillan's Unfolding Algorithm 7
(a)


2. A 1-safe net system, its unfolding, and a prefix
The procedure does not necessarily terminate. In fact, it terminates if and
only if the input system \Sigma does not have any infinite occurrence sequence.
It will eventually produce any reachable marking only under the fairness
assumption that every event added to pe is eventually chosen to extend
Unf (the correctness proof follows easily from the definitions and from the
results of [4]).
Constructing a Finite Complete Prefix
We say that a branching process fi of a net system \Sigma is complete if for every
reachable marking M there exists a configuration C in fi such that:
ffl Mark (i.e., M is represented in fi), and
ffl for every transition t enabled by M there exists a configuration C[feg
such that
2 C and e is labelled by t.
The unfolding of a net system is always complete. A complete prefix
contains as much information as the unfolding, in the sense that we can
construct the unfolding from it as the least fixpoint of a suitable operation.
This property does not hold if we only require every reachable marking
to be represented. For instance, the net system of Figure 2(a) has Figure
2(b) as unfolding. Figure 2(c) shows a prefix of the unfolding in which
every reachable marking is represented. The prefix has lost the information
indicating that t 2 can occur from the initial marking. Observe that the
prefix is not complete.
Since an n-safe net system has only finitely many reachable markings,
its unfolding contains at least one complete finite prefix. We transform the
algorithm above into a new one whose output is such a prefix.
We need some preliminary notations and definitions:
Given a configuration C, we denote by C \Phi E the fact that C [ E is a
configuration such that C " We say that is an extension of
C, and that E is a suffix to C. Obviously, if C ae C 0 then there is a suffix
of C such that C \Phi
Let C 1 and C 2 be two finite configurations such that Mark (C 1
It follows easily from the definitions that * Cut(C i ) is isomorphic to the
8 J. Esparza, S. R-omer, W. Vogler
unfolding of \Sigma
are isomorphic. Moreover, there is an isomorphism I C2
C1 from *Cut(C 1 ) to
*Cut (C 2 ). This isomorphism induces a mapping from the finite extensions
of C 1 onto the extensions of
C1 (E).
We can now introduce the three basic notions of the algorithm:
Definition 3.3
A partial order OE on the finite configurations of a branching process
is an adequate order if:
ffl OE is well-founded,
ffl OE refines ae, i.e. C
ffl OE is preserved by finite extensions, meaning that if C 1 OE C 2 and
C1 (E).Definition 3.4 Local configuration
The local configuration [e] of an event of a branching process is the set
of events e 0 such that e 0 - e. 2 3.4
Definition 3.5 Cut-off event
Let fi be a branching process and let OE be an adequate partial order
on the configurations of fi. An event e is a cut-off event (with respect
to OE) if fi contains a local configuration [e 0 ] such that
(a)
(b) [e].The new algorithm has as parameter an adequate order OE, i.e. every
different adequate order leads to a different algorithm.
Algorithm 3.6 The complete finite prefix algorithm
input: An n-safe net system g.
output: A complete finite prefix Fin of Unf.
begin
Fin
pe := PE
cut-off := ;;
2 It is immediate to prove that [e] is a configuration.
An Improvement of McMillan's Unfolding Algorithm 9
while pe 6= ; do
choose an event in pe such that [e] is minimal
with respect to OE;
if [e]"
append to Fin the event e and a condition
(s; e) for every output place s of t;
pe := PE
if e is a cut-off event of Fin then
cut-off := cut-off [feg
endif
else pe := pe n feg
endif
endwhile
endMcMillan's algorithm in [10] corresponds to the order
It is easy to see that OE m is adequate.
The reason of condition (a) in the definition of cut-off event is intuitively
clear in the light of this algorithm. Since Mark ([e 0 Mark([e]), the continuations
of Unf from Cut([e]) and Cut([e 0 ]) are isomorphic. Then, loosely
speaking, all the reachable markings that we find in the continuation of
Unf from Cut([e]) are already present in the continuation from Cut([e 0 ]),
and so there is no need to have the former in Fin. The r-ole of condition
(b) is more technical. In fact, when McMillan's algorithm is applied to
"ordinary" small examples, condition (b) seems to be superfluous, and the
following strategy seems to work: if an event e is added and Fin already
contains a local configuration [e 0 ] such that Mark
mark e as cut-off event. The following example (also independently found
by K. McMillan) shows that this strategy is incorrect. Consider the 1-safe
net system of Figure 3.
The marking fs 12 g is reachable. Without condition (b) we can generate
the prefix of Figure 4.
The names of the events are numbers which indicate the order in which
they are added to the prefix. The events 8 and 10 are cut-off events, because
their corresponding markings fs 7 are also
the markings corresponding to the events 7 and 9, respectively. This prefix
is not complete, because fs 12 g is not represented in it.
Observe that Fin contains all the events of the set cut-off. We could
modify the algorithm to remove all these events, and the prefix so obtained
would still enjoy the property that every reachable marking is represented
in it. However, the prefix would not be necessarily complete. Consider for
J. Esparza, S. R-omer, W. Vogler


3. A 1-safe net system
example the net system of Figure 2(a). Algorithm 3.6 generates the branching
process of Figure 2(b), and one of the two events of the process (the
maximal one with respect to OE) is a cut-off event. If this event is removed,
we obtain an incomplete prefix.
We now prove the correctness of Algorithm 3.6.
Proposition 3.7
Fin is finite.
Proof: Given an event e of Fin, define the depth of e as the length of a
longest chain of events
the depth of e is denoted by d(e). We prove the
following results:
(1) For every event e of Fin, d(e) is the number
of reachable markings of \Sigma.
Since cuts correspond to reachable markings, every chain of
events contains two events e i ,
and OE refines ae, we have is a cut-off
event of Unf. Should the finite prefix algorithm generate e j ,
then it has generated e i before and e j is recognized as a cut-off
event of Fin, too.
(2) For every event e of Fin, the sets ffl e and e ffl are finite.
By the definition of homomorphism, there is a bijection between
denotes the homomorphism of
Fin, and similarly for ffl p(e) and p( ffl e). The result follows from
the finiteness of N .
An Improvement of McMillan's Unfolding Algorithm 11


4. A prefix of the net system of Figure 3
(3) For every k - 0, Fin contains only finitely many events e such
that d(e) - k.
By complete induction on k. The base case,
be the set of events of depth at most k. We prove that if
g.
By (2) and the induction hypothesis,
k is finite. Since ffl E k+1 '
we get by property (ii) in the definition of a
branching process that E k+1 is finite.
It follows from (1) and (3) that Fin only contains finitely many
events. By (2) it contains only finitely many conditions. 3.7
Proposition 3.8
Fin is complete.
Proof: We first prove that every reachable marking of \Sigma is represented in
Fin.
Let M be an arbitrary reachable marking of \Sigma. There exists a
configuration C of Unf such that Mark If C is not a
configuration of Fin, then it contains some cut-off event e, and so
set of events E. By the definition of a cut-off
event, there exists a local configuration [e 0 ] such that [e 0 ] OE [e] and
Mark ([e 0
Consider the configuration C
[e] (E). Since OE is preserved
by finite extensions, we have C 0 OE C. Morever, Mark(C 0
C 0 is not a configuration of Fin, then we can iterate the procedure
J. Esparza, S. R-omer, W. Vogler
and find a configuration C 00 such that C 00 OE C 0 and Mark (C 00
The procedure cannot be iterated infinitely often because OE is well-
founded. Therefore, it terminates in a configuration of Fin.
Now we show that Fin is complete. We have to prove that for every
reachable marking M there exists a configuration C in fi such that:
ffl for every transition t enabled by M there exists a configuration
2 C and e is labelled by t.
Let M be an arbitrary reachable marking of \Sigma. Since M is represented
in Fin, the set of configurations C of Fin satisfying Mark(C)
nonempty. By well-foundedness, this set has at least a minimal
element Cm with respect to OE. If Cm would contain some cut-off
event, then we would find as above another configuration C 0 satisfying
which contradicts the minimality
of Cm . So Cm contains no cut-off event.
Let t be an arbitrary transition enabled by M . Then there exists a
configuration Cm [ feg of Unf such that
2 Cm and e is labelled
by t. Assume that Cm [ feg is not a configuration of Fin. Since
Fin contains all the events of the set cut-off in Algorithm 3.6, it
also contains a cut-off event e 0 ! e. This implies e 0 2 Cm , which
contradicts that Cm contains no cut-off event. So Cm [ feg is a
configuration of Fin. 3.8
4 An Adequate Order for the 1-Safe Case
As we mentioned in the introduction, McMillan's algorithm may be inefficient
in some cases. An extreme example, due to Kishinevsky and Taubin,
is the family of systems on the left of Figure 5.
While a minimal complete prefix has size O(n) in the size of the system
(see the dotted line in Figure 5), the branching process generated by
McMillan's algorithm has size O(2 n ). The reason is that, for every marking
M , all the local configurations [e] satisfying have the same
size, and therefore there exist no cut-off events with respect to McMillan's
Our parametric presentation of Algorithm 3.6 suggests how to improve
this: it suffices to find a new adequate order OE r that refines McMillan's
. Such an order induces a weaker notion of cut-off event; more
precisely, every cut-off event with respect to OE m is also a cut-off event
with respect to OE r , but maybe not the other way round. Therefore, the
instance of Algorithm 3.6 which uses the new order generates at least as
many cut-off events as McMillan's instance, and maybe more. In the latter
case, Algorithm 3.6 generates a smaller prefix.
An Improvement of McMillan's Unfolding Algorithm 13
sk
sk sk sk sk
copies of sk
Minimal
complete
prefix


5. A Petri net and its unfolding
The order OE r is particularly good if in addition it is total. In this case,
whenever an event e is generated after some other event e 0 such that
Mark [e] (because events are generated
in accordance with the total order OE r ), and so e is marked as a cut-off
event. So we have the following two properties:
ffl the guard "e is a cut-off event of Fin" in the inner if instruction of
Algorithm 3.6 can be replaced by "Fin contains a local configuration
ffl the number of events of the complete prefix which are not cut-off
events cannot exceed the number of reachable markings.
In the sequel, let fixed net system, and let - be an
arbitrary total order on the transitions of \Sigma. We extend - to a partial order
on sets of events of a branching process as follows: for a set E of events, let
'(E) be that sequence of transitions which is ordered according to - and
contains each transition t as often as there are events in E with label t. Now
we say that they have the same
length but '(E 1 ) is lexicographically smaller than '(E 2 ). Note that E 1 and
are incomparable with respect to - iff In particular, if
are incomparable with respect to -, then jE
We now define OE r more generally on suffixes of configurations of a
branching process (recall that a set of events E is a suffix of a configuration
if there exists a configuration C such that C \Phi E).
Definition 4.1 Total order OE r
be two suffixes of configurations of a branching process
fi and let Min(E 1 ) and Min(E 2 ) denote the sets of minimal elements
of with respect to the causal relation. We say
14 J. Esparza, S. R-omer, W. Vogler
).Notice that this definition would not be correct for configurations only,
because need not be a configuration even if E is one.
The second condition of this definition could be expressed as: the Foata-
Normal-Form of E 1 is smaller than that of E 2 with respect to -, cf. e.g.
[3].
Theorem 4.2
Let fi be a branching process of a 1-safe net system. OE r is an adequate
total order on the configurations of fi.
Proof: a) OE r is a partial order.
It is easy to see by induction on jEj that OE r is irreflexive. Now
assume
For such triples with these equalities we apply induction on the
otherwise we apply induction to E i n Min(E i ),
which are also suffixes of configurations.
r is total on configurations.
Assume that C 1 and C 2 are two incomparable configurations, i.e.
prove by induction on jC 1
The base case gives C
We first prove Min(C 1 Assume without loss of generality
that
contains an event e 2 such that p(e 1
and ffl Min(C 2 ) are subsets of Min(N ), and all the conditions of
different labels by Proposition 2.1, we have ffl e
This contradicts condition (ii) of the definition of branching process.
are configurations of the branching process *Cut(Min(C 1 )) of
(Proposition 2.2); by induction we conclude
c) OE r is well-founded.
In a sequence C the size of the C i cannot decrease
infinitely often; also, for configurations of the same size,
An Improvement of McMillan's Unfolding Algorithm 15
decrease infinitely often with respect to -, since the
sequences are drawn from a finite set; an analogous statement
holds for Min(C i ). Hence, we assume that all jC i j, all '(C i )
and all '(Min(C i are equal and apply induction on the common
size. For jC 0, an infinite decreasing sequence is impos-
sible. Otherwise, we conclude as in case b) that we would have
which is
impossible by induction.
d) OE r refines ae.
Obvious.
OE r is preserved by finite extensions.
This is the most intricate part of the proof, and here all the complications
in Definition 4.1 come into play. Take C 1 OE r C 2 with
Mark We have to show that C 1 \Phi
I C2
C1 (E), and we can assume that apply induction af-
terwards. The case C 1 - C 2 is easy, hence assume '(C 1
and in particular jC show first that e is minimal in
only if I C2
C1 (e) is minimal in C 0
(e)g.
let e be minimal in C 0
i.e. the transition p(e) is enabled under
the initial marking. Let s 2 ffl p(e); then no condition in ffl
1 is
labelled s, since these conditions would be in co relation with the
s-labelled condition in ffl e, contradicting Proposition 2.1. Thus, C 1
contains no event e 0 with s 2 ffl p(e 0 ), and the same holds for C 2 since
Therefore, the conditions in Cut(C 2 ) with label in
ffl p(e) are minimal conditions of fi, and I C2
.
The reverse implication holds analogously, since about C 1 and C 2
we have only used the hypothesis '(C
With this knowledge about the positions of e in C 0
1 and I C2
C1 (e) in C 0
we proceed as follows. If then we now see that
so we are done. If '(Min(C 1
and e 2 Min(C 0
hence C 0
2 . Finally, if '(Min(C 1
1 ), we again argue that Min(C 1
are configurations of the branching
process with an inductive
argument we get C 0
are also done
in this case. 4.2
We close this section with a remark on the minimality of the prefixes
generated by the new algorithm, i.e. by Algorithm 3.6 with OE r as adequate
order.

Figure

1(b) and (c) are a minimal complete prefix and the prefix
J. Esparza, S. R-omer, W. Vogler
generated by the new algorithm for the 1-safe system of Figure 1(a), re-
spectively. It follows that the new algorithm does not always compute a
minimal complete prefix.
However, the prefixes computed by the algorithm are minimal in another
sense. The algorithm stores only the reachable markings corresponding to
local configurations, which for the purpose of this discussion we call local
markings. This is the feature which makes the algorithm interesting for
concurrent systems: the local markings can be a very small subset of the
reachable markings, and therefore the storage of the unfolding may require
much less memory than the storage of the state space. In order to find out
that the prefix of Figure 1(b) is complete, we also need to know that the
initial marking fs appears again in the prefix as a non-local marking.
If we only store information about local markings, then the prefix of Figure
1(c) is minimal, as well as all the prefixes generated by the new algorithm.
The reason is the observation made above: all the local configurations of
Fin which are not induced by cut-off events correspond to different mark-
ings; therefore, in a prefix smaller than Fin we lose information about the
reachability of some marking.
5 Implementation Issues and Experimental Results
The implementation of the Algorithm 3.6 has been carried out in the context
of the model checker described in [5], which allows to efficiently verify
formulae expressed in a simple branching time temporal logic.
For the storage of Petri nets and branching processes we have developed
an efficient, universal data structure that allows fast access to single nodes
[14]. This data structure is based on the underlying incidence matrix of the
net. Places, transitions and arcs are represented by nodes of doubly linked
lists to support fast insertion and deletion of single nodes.
The computation of new elements for the set PE involves the combinatorial
problem of finding sets of conditions B such that
transition t. We have implemented several improvements in this combinatorial
determination, which have significant influence on the performance
of the algorithm. The interested reader is referred to [6].
Algorithm 3.6 is very simple, and can be easily proved correct, but is not
efficient. In particular, it computes the set PE of possible extensions each
time a new event is added to Fin, which is clearly redundant. Similarly to
McMillan's original algorithm [10], in the implementation we use a queue to
store the set PE of possible extensions. The new events of Fin are extracted
from the head of this list, and, when an event is added, the new possible
extensions it generates are appended to its tail.
The simplest way to organize the list would be to sort its events according
to the total order OE r . However, this is again inefficient, because it involves
An Improvement of McMillan's Unfolding Algorithm 17


6. n-buffer for
Original net Unfolding time [s]


1. Results of the n buffer example 3 .
performing unneccessary comparisons. The solution is to sort the events
according to the size of their local configuration, as in [10], and compare
events with respect to OE r only when it is really needed.
With this implementation, the new algorithm only computes more than
McMillan's when two events e and e 0 satisfy
]j. But this is precisely the case in which the algorithm behaves
better, because it always identifies either e or e 0 as a cut-off event. In
other words: when the complete prefix computed by McMillan's algorithm
is minimal, our algorithm computes the same result with no time overhead.
The running time of the new algorithm is O(( jBj
is the set of
conditions of the unfolding, and - denotes the maximal size of the presets
of the transitions in the original net (notice that this is not a measure in
the size of the input). The dominating factor in the time complexity is the
computation of the possible extensions. The space required is linear in the
size of the unfolding because we store a fixed amount of information per
event.
Finally, we present some experimental results on three scalable exam-
ples. We compare McMillan's algorithm and the new algorithm, both implemented
using the universal data structure and the improvements in the
combinatorial determination mentioned above.
The first example is a model of a concurrent n-buffer (see Figure 5). The
net has 2n places and is the buffer's capacity.
While the number of reachable markings is 2 n , Fin has size O(n 2 ) and contains
one single cut-off event (see Table 1). In this example, the complete
prefix computed by McMillan's algorithm is minimal. The new algorithm
computes the same prefix without time overhead, as expected.
Our second example, Figure 5, is a model of a slotted ring protocol taken
from [13]. Here the size of the prefix produced by the new algorithm grows
J. Esparza, S. R-omer, W. Vogler
GiveFreeSlot1 P11 GiveFreeSlot2 P12 Free2
Used2
GoOn2
Owner2
Used1
Other1
GoOn1
Other2


7. Slotted ring protocol for 2.
Original net McMillan's algorithm New algorithm
9 90 90 3:8


2. Results of the slotted ring protocol example;
more slowly than in the case of McMillan's algorithm. For the output
is already one order of magnitude smaller. The slow growth in size can cause
an even more dramatic reduction in the running time.
Original net McMillan's algorithm New algorithm
43 94 44 8 0:02 52 23 4 0:00
9 71 53 7423 5686 2834 512 22:90


3. Results of Milner's cyclic
In

Table

3, we give the times for an example taken from [2] that models
Milner's cyclic scheduler for n tasks. While the size of the unfolding produced
by the McMillan's algorithm grows exponentially with the number
of tasks, we get linear size using our new one.
3 All the times have been measured on a SPARCstation 20 with 48 MB main memory.
4 These times could not be calculated; for we interrupted the computation after
more than 12 hours.
An Improvement of McMillan's Unfolding Algorithm 19
6 Conclusions
We have presented an algorithm for the computation of a complete finite
prefix of an unfolding. We have used a refinement of McMillan's basic notion
of cut-off event. The prefixes constructed by the algorithm contain at most
non-cut-off events, where n is the number of reachable markings of the
net. Therefore, we can guarantee that the prefix is never larger than the
reachability graph, which does not hold for the algorithm of [10].
Recently, Kondratyev et al. have independently found another partial
order between events which permits to obtain reduced unfoldings [9]. Their
technique works for bounded nets. However, the partial order is not total,
and so the upper bound on the size of the unfolding cannot be derived.

Acknowledgements

We thank Michael Kishinevsky, Alexander Taubin and Alex Yakovlev for
drawing our attention to this problem, Burkhard Graves for detecting some
mistakes, and an anonymous referee for helpful comments.



--R

Nonsequential Processes - A Petri Net View
Evaluating Deadlock Detection Methods.
Combinatorics on Traces.
Branching processes of Petri nets.
Model Checking Using Net Unfoldings.
An improvement of McMillan's unfolding algorithm.
Concurrent Hardware: The Theory and Practice of Self-Timed Design
Verification of speed-independent circuits by STG unfoldings
Analysis of Petri Nets by Ordering Relations.
A Technique of a State Space Search Based on Unfolding.
Trace theoretic verification of asynchronous circuits using unfoldings.
Petri Nets
Petri Net Analysis Using Boolean Manipulation.
Implementation of a Compositional Partial Order Semantics of Petri Boxes.
--TR
Combinatorics on traces
Branching processes of Petri nets
Executions: a new partial-order semantics of Petri nets
Model checking using net unfoldings
A technique of state space search based on unfolding
An Improvement of McMillan''s Unfolding Algorithm
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings
Petri Net Analysis Using Boolean Manipulation
Calculating Place Capacity for Petri Nets Using Unfoldings

--CTR
Alessandro Giua , Xiaolan Xie, Control of Safe Ordinary Petri Nets Using Unfolding, Discrete Event Dynamic Systems, v.15 n.4, p.349-373, December  2005
Victor Khomenko , Maciej Koutny, Verification of bounded Petri nets using integer programming, Formal Methods in System Design, v.30 n.2, p.143-176, April     2007
Victor Khomenko , Maciej Koutny , Alex Yakovlev, Logic synthesis for asynchronous circuits based on STG unfoldings and incremental SAT, Fundamenta Informaticae, v.70 n.1, p.49-73, March 2006
Victor Khomenko , Maciej Koutny , Alex Yakovlev, Logic Synthesis for Asynchronous Circuits Based on STG Unfoldings and Incremental SAT, Fundamenta Informaticae, v.70 n.1,2, p.49-73, April 2006
Victor Khomenko , Maciej Koutny , Alex Yakovlev, Detecting State Encoding Conflicts in STG Unfoldings Using SAT, Fundamenta Informaticae, v.62 n.2, p.221-241, April 2004
Fabre, Trellis Processes: A Compact Representation for Runs of Concurrent Systems, Discrete Event Dynamic Systems, v.17 n.3, p.267-306, September 2007
Stefan Haar, Probabilistic cluster unfoldings, Fundamenta Informaticae, v.53 n.3,4, p.281-314, December 2002
Stefan Haar, Probabilistic Cluster Unfoldings, Fundamenta Informaticae, v.53 n.3-4, p.281-314, August 2002
partial-order semantics;petri nets;unfolding