Structural Methods to Improve the Symbolic Analysis of Petri Nets

  • Enric Pastor
  • Jordi Cortadella
  • Marco A. Peña
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1639)


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.


Boolean Variable Encode Function Symbolic Analysis Dine Philosopher Reachable Marking 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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
  2. [2]
    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
  3. [3]
    F. M. Brown. Boolean Reasoning: The Logic of Boolean Equations. Kluwer Academic Publishers, 1990.Google Scholar
  4. [4]
    R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  5. [5]
    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
  6. [6]
    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
  7. [7]
    J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, Cambridge, Great Britain, 1995.zbMATHGoogle Scholar
  8. [8]
    J. Desel, K.P. Neuendorf, and M.D. Radola. Proving nonreachability by moduloinvariants. Theoretical Computer Science, (153):49–64, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In Proc. DAC, 1982.Google Scholar
  10. [10]
    M. Hack. Analysis of production schemata by Petri nets. M.s. thesis, MIT, February 1972.Google Scholar
  11. [11]
    G. J. Holzmann. An Improved Protocol Reachability Analysis Technique Software Practice and Experience, 18(2):137–161, 1988.CrossRefGoogle Scholar
  12. [12]
    R. Kannan and A. Bachem. Polynomial algorithms for computing the smith and hermite normal forms of an integer matrix. SIAM J. Comput., 4(8):499–577, 1979.CrossRefMathSciNetGoogle Scholar
  13. [13]
    K. Lautenbach. Linear algebraic techniques for place/transition nets. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, volume 254 of LNCS, pages 142–167. Springer-Verlag, 1987.CrossRefGoogle Scholar
  14. [14]
    E. J. McCluskey. Minimization of boolean functions. Bell Syst. Technical Journal, (35):1417–1444, November 1956.MathSciNetGoogle Scholar
  15. [15]
    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
  16. [16]
    Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–574, April 1989.CrossRefGoogle Scholar
  17. [17]
    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
  18. [18]
    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
  19. [19]
    T. Yoneda, H. Hatori, A. Takahara, and S. Minato. BDDs vs. Zero-Suppressed BDDs: for CTL symbolic model checking of petri nets. In Proc. of Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 435–449. Springer-Verlag, 1996.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Enric Pastor
    • 1
  • Jordi Cortadella
    • 2
  • Marco A. Peña
    • 1
  1. 1.Department of Computer ArchitectureUniversitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.Department of SoftwareUniversitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations