Abstract
This paper presents a new method for computing reduced representation of vector state spaces consisting of infinitely many states. Petri nets are used as a model for generating vector state spaces, and the state space is represented in the form of semilinear subsets of vectors. By combining the partial order methods with the proposed algorithm, we can compute reduced state spaces which preserve some important properties, such as liveness of each transition and the existence of deadlocks. The state space of a finite capacity system can be viewed as that of an infinite capacity system projected to the states satisfying the capacity condition. We also show that the proposed algorithm is applicable to vector state spaces with finite capacities.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
S.B. Akers: Binary Decision Diagrams, IEEE Trans. Computers, C-27-6, 509–516 (1978).
R.E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Computers, C35-8, 677–691 (1986).
J.R. Burch, E.M. Clarke, K.L. McMillan: Sequential Circuit Verification Using Symbolic Model Checking, 27th ACM/IEEE Design Automation Conference, 46–51 (1990).
P. Godfroid: Using Partial Orders to Improve Automatic Verification Methods, Lecture Notes in Computer Sience, No. 531, 176–185 (1990).
P. Godefroid, P. Wolper: Using Partial Orderes for the Efficient Verification of Deadlock Treedom and Safety Properties, Lecture Notes in Computer Sience, No. 575, 332–342 (1991).
K. Hiraishi, A. Ichikawa: On Structural Conditions for Weak Persistency and Semilinearity of Petri Nets, Theoretical Computer Science, Vol. 93, 185–199 (1992).
K. Hiraishi, M. Makano: On Symbolic Model Checking in Petri Nets, OEICE Trans. Vol. E77-A, No. 10, 1602–1606 (1995).
C. A. R. Hoare: Communicating Sequential Processes, Prentice Hall International Series in Computer Science, Prentice Hall, 1985.
R. M. Karp and R. E. Miller: Parallel Program Schemata, J. Computer and System Science, Vol. 3, No. 2, 147–195, 1969.
T. Murata: Petri Nets: Properties, Analysis and Applications, Proc. of the IEEE, Vol. 77, No. 4 (1989).
E. Pastor, Oriol Roig, J. Cortadella, and R. Badia: Petri Net Analysis Using Boolean Manipulation, Lecture Notes in Computer Sience, No. 815, Springer-Verlag, 416–435 (1994).
J. L. Peterson: Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
M. Tiusanen: Symbolic, Symmetry, and Stubborn Set Searches, Lecture Notes in Computer Sience, No. 815, Springer-Verlag, 511–530 (1990).
A. Valmari: Stubborn Sets for Reduced State Space Generation, Lecture Notes in Computer Sience, No. 483, Springer-Verlag, 491–515 (1990).
A. Valmari: On-the-fly Verification with Stubborn Sets, Lecture Notes in Computer Sience, No. 697, Springer-Verlag, 397–408 (1993).
P. Wolper, P. Godefroid, D. Pirottin: A Tutorial on Partial-Order Methods for the Verification of Concurrent Systems, Computer Aided Verification '93 Tutorial (1993).
H. Yamasaki: On Weak Persistency of Petri Nets, Information Processing letters, Vol.13, No.3, 94–97, (1981).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hiraishi, K. (1996). Reduced state space representation for unbounded vector state spaces. In: Billington, J., Reisig, W. (eds) Application and Theory of Petri Nets 1996. ICATPN 1996. Lecture Notes in Computer Science, vol 1091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61363-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-61363-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61363-3
Online ISBN: 978-3-540-68505-0
eBook Packages: Springer Book Archive