Advertisement

Efficient Reachability Set Generation and Storage Using Decision Diagrams

  • Andrew S. Miner
  • Gianfranco Ciardo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1639)

Abstract

We present a new technique for the generation and storage of the reachability set of a Petri net. Our approach is inspired by previous work on Binary and Multi-valued Decision Diagrams but exploits a concept of locality for the effect of a transition’s firing to vastly improve algorithmic performance. The result is a data structure and a set of manipulation routines that can be used to generate and store enormous sets extremely efficiently in terms of both memory and execution time.

Classiffication: Reachability set generation. System veriffication. Computer tools.

Keywords

Boolean Function Local Transition Binary Decision Diagram Kanban System Dine Philosopher 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    S. C. Allmaier, M. Kowarschik, and G. Horton. State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor. In Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM’97), pages 112–121, St. Malo, France, June 1997. IEEE Comp. Soc. Press.Google Scholar
  2. 2.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp., 35(8):677–691, Aug. 1986.zbMATHCrossRefGoogle Scholar
  3. 3.
    R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv., 24(3):393–318, 1992.CrossRefGoogle Scholar
  4. 4.
    P. Buchholz. Hierarchical structuring of superposed GSPNs. In Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM’97), pages 81–90, St. Malo, France, June 1997. IEEE Comp. Soc. Press.Google Scholar
  5. 5.
    P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of Kronecker operations on sparse matrices with applications to the solution of Markov models. ICASE Report 97-66 (NASA/CR-97-206274), Institute for Computer Applications in Science and Engineering, Hampton, VA, 1997. Submitted for publication.Google Scholar
  6. 6.
    G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In R. Valette, editor, Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815 (Proc. 15th Int. Conf. on Applications and Theory of Petri Nets, Zaragoza, Spain), pages 179–198. Springer-Verlag, June 1994.Google Scholar
  7. 7.
    G. Ciardo and A. S. Miner. SMART: Simulation and Markovian Analyzer for Reliability and Timing. In Proc. IEEE International Computer Performance and Dependability Symposium (IPDS’96), page 60, Urbana-Champaign, IL, USA, Sept. 1996. IEEE Comp. Soc. Press.Google Scholar
  8. 8.
    G. Ciardo and A. S. Miner. Storage alternatives for large structured state spaces. In R. Marie, B. Plateau, M. Calzarossa, and G. Rubino, editors, Proc. 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, LNCS 1245, pages 44–57, St. Malo, France, June 1997. Springer-Verlag.CrossRefGoogle Scholar
  9. 9.
    G. Ciardo and M. Tilgner. On the use of Kronecker operators for the solution of generalized stochastic Petri nets. ICASE Report 96-35, Institute for Computer Applications in Science and Engineering, Hampton, VA, May 1996.Google Scholar
  10. 10.
    S. Donatelli. Superposed generalized stochastic Petri nets: definition and efficient solution. In R. Valette, editor, Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815 (Proc. 15th Int. Conf. on Applications and Theory of Petri Nets), pages 258–277, Zaragoza, Spain, June 1994. Springer-Verlag.Google Scholar
  11. 11.
    T. Kam. State Minimization of Finite State Machines using Implicit Techniques. PhD thesis, University of California at Berkeley, 1995.Google Scholar
  12. 12.
    P. Kemper. Numerical analysis of superposed GSPNs. IEEE Trans. Softw. Eng., 22(4):615–628, Sept. 1996.CrossRefMathSciNetGoogle Scholar
  13. 13.
    P. Kemper. Reachability analysis based on structured representations. In J. Billington and W. Reisig, editors, Application and Theory of Petri Nets 1996, Lecture Notes in Computer Science 1091 (Proc. 17th Int. Conf. on Applications and Theory of Petri Nets, Osaka, Japan), pages 269–288. Springer-Verlag, June 1996.Google Scholar
  14. 14.
    C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell Syst. Techn. J., 38(4):985–999, July 1959.Google Scholar
  15. 15.
    E. Pastor and J. Cortadella. Efficient encoding schemes for symbolic analysis of Petri nets. In Proc. Design Automation and Test in Europe, Feb. 1998.Google Scholar
  16. 16.
    E. Pastor and J. Cortadella. Structural methods applied to the symbolic analysis of Petri nets. In Proc. IEEE/ACM International Workshop on Logic Synthesis, June 1998.Google Scholar
  17. 17.
    E. Pastor, O. Roig, J. Cortadella, and R. Badia. Petri net analysis using boolean manipulation. In R. Valette, editor, Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815 (Proc. 15th Int. Conf. on Applications and Theory of Petri Nets, Zaragoza, Spain), pages 416–435. Springer-Verlag, June 1994.Google Scholar
  18. 18.
    O. Roig, J. Cortadella, and E. Pastor. Verification of asynchronous circuits by BDD-based model checking of Petri nets. In G. De Michelis and M. Diaz, editors, Application and Theory of Petri Nets 1995, Lecture Notes in Computer Science 935 (Proc. 16th Int. Conf. on Applications and Theory of Petri Nets, Turin, Italy), pages 374–391. Springer-Verlag, June 1995.Google Scholar
  19. 19.
    A. Srinivasan, T. Kam, S. Malik, and R. K. Brayton. Algorithms for discrete function manipulation. In International Conference on CAD, pages 92–95. IEEE Computer Society, 1990.Google Scholar
  20. 20.
    D. Zampunièris. The Sharing Tree Data Structure, Theory and Applications in Formal Verification. PhD thesis, Department of Computer Science, University of Namur, Belgium, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Andrew S. Miner
    • 1
  • Gianfranco Ciardo
    • 1
  1. 1.Department of Computer ScienceCollege of William and Mary WilliamsburgVA

Personalised recommendations