Efficient Encoding Schemes for Symbolic Analysis of Petri Nets

Petri nets are a graph-based formalism appropriate to model concurrentsystems such as asynchronouscircuits or network protocols. Symbolic techniques based on Binary Decision Diagrams (BDDs) have emerged as one of the strategies to overcome the state explosion problem in the analysis ofsystems modeled byPetri nets. The existing techniques for state encoding use a variableper-place strategy that leads to encoding schemes with very low density. This drawback has been partially mitigated by using Zero-Suppressed BDDs, that provide a typical reduction of BDD sizes by a factor of two. This work presents novel encoding schemes for Petri nets. By using algebraic techniques to analyze the topology of the net, sets of places "structurally related" can be derived and encoded by only using a logarithmic number of boolean variables. Such approach allows to drastically decrease the number of variables for state encoding and reduce memory and CPU requirements significantly.

• Type: Conference
• Year: 1998
• Where: DATE
• Authors: Enric Pastor, Jordi Cortadella
• Keywords: Binary Decision Diagrams, DATE 1998, Hardware, Petri Nets, State Encoding