Structural Methods to Improve the Symbolic Analysis of Petri Nets
Symbolic techniques based on BDDs (Binary Decision Diagrams) have emerged as an efficient strategy for the analysis of Petri nets. The existing techniques for the symbolic encoding of each marking use a fixed set of variables per place, leading to encoding schemes with very low density. This drawback has been previously mitigated by using Zero-Suppressed BDDs, that provide a typical reduction of BDD sizes by a factor of two. Structural Petri net theory provides P-invariants that help to derive more efficient encoding schemes for the BDD representations of markings. P-invariants also provide a mechanism to identify conservative upper bounds for the reachable markings. The unreachable markings determined by the upper bound can be used to alleviate both the calculation of the exact reachability set and the scrutiny of properties. Such approach allows to drastically decrease the number of variables for marking encoding and reduce memory and CPU requirements significantly.
KeywordsBoolean Variable Encode Function Symbolic Analysis Dine Philosopher Reachable Marking
Unable to display preview. Download preview PDF.
- R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In Proc. ICCAD, pages 188–191, November 1993.Google Scholar
- K. S. Brace, R. E. Bryant, and R. L. Rudell. Efficient implementation of a BDD package. In Proc. DAC, pages 40–45, 1990.Google Scholar
- F. M. Brown. Boolean Reasoning: The Logic of Boolean Equations. Kluwer Academic Publishers, 1990.Google Scholar
- Jerry R. Burch, Edmund M. Clarke, D. E. Long, Kenneth L. McMillan, and David L. Dill. Symbolic model checking for sequential circuit verification. IEEE Trans. on CAD, 13(4):401–424, 1994.Google Scholar
- G. Chiola Compiling Techniques for the Analysis of Stochastic Petri Nets. In 4th Int. Conf. on Modeling Techniques and Tools for Computer Performance Evaluation, pages 11–24, September 1989.Google Scholar
- C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In Proc. DAC, 1982.Google Scholar
- M. Hack. Analysis of production schemata by Petri nets. M.s. thesis, MIT, February 1972.Google Scholar
- G. Memmi and G. Roucairol. Linear algebra in net theory. In W. Brauer, editor, Net Theory and Applications, volume 84 of LNCS, pages 213–223. Springer-Verlag, 1980.Google Scholar
- E. Pastor and J. Cortadella. Efficient encoding schemes for symbolic analysis of petri nets. In Proc. Design, Automation and Test in Europe, pages 790–795, Paris (France), February 1998.Google Scholar
- E. Pastor, O. Roig, J. Cortadella, and R. M. Badia. Petri net analysis using boolean manipulation. In 15th Int. Conf. on Application and Theory of Petri Nets, volume 815 of LNCS, pages 416–435. Springer-Verlag, June 1994.Google Scholar