Petri Net Unfoldings, also known as Finite Prefix, have been
used as an analysing tool for Petri Net models of asynchronous
system designs. Such a technique is used to investigate the properties
of the models such as safeness, liveness, etc. One of the advantages
of this technique over other analysing methods, such as reachability
graphs or symbolic traversals, is that it does not suffer from
a 'state-space explosion' problem. However, a major problem is
still faced with the construction of 'complete-minimum' unfoldings
for a certain class of nets, namely non read persistent nets.
An alternative solution to this is by introducing a notion of
'overlay' in the construction algorithm of the unfoldings.