Postgraduate Conference Abstract


Alamsyah, F Year 2

Unfoldings of Non Read Persistent Nets

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.