Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
K. S. Brace, R. E. Bryant, and R. L. Rudell. Efficient implementation of a BDD package. In Proc. DAC, pages 40–45, 1990.
F. M. Brown. Boolean Reasoning: The Logic of Boolean Equations. Kluwer Academic Publishers, 1990.
R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
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.
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.
J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, Cambridge, Great Britain, 1995.
J. Desel, K.P. Neuendorf, and M.D. Radola. Proving nonreachability by moduloinvariants. Theoretical Computer Science, (153):49–64, 1996.
C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In Proc. DAC, 1982.
M. Hack. Analysis of production schemata by Petri nets. M.s. thesis, MIT, February 1972.
G. J. Holzmann. An Improved Protocol Reachability Analysis Technique Software Practice and Experience, 18(2):137–161, 1988.
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.
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.
E. J. McCluskey. Minimization of boolean functions. Bell Syst. Technical Journal, (35):1417–1444, November 1956.
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.
Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–574, April 1989.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pastor, E., Cortadella, J., Peña, M.A. (1999). Structural Methods to Improve the Symbolic Analysis of Petri Nets. In: Donatelli, S., Kleijn, J. (eds) Application and Theory of Petri Nets 1999. ICATPN 1999. Lecture Notes in Computer Science, vol 1639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48745-X_3
Download citation
DOI: https://doi.org/10.1007/3-540-48745-X_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66132-0
Online ISBN: 978-3-540-48745-6
eBook Packages: Springer Book Archive