Abstract
Exploration of the reachability set (RS) is one of the crucial building blocks for various analysis methods ranging from model checking to Markov chain (MC) based performance analysis. In the context of MCs, structured representations of state transition matrices using tensor (Kronecker) algebra have been successfully employed to handle the impact of the state space explosion problem. In this paper such structured representations give rise to a new RS exploration algorithm for superposed generalized stochastic Petri nets and stochastic automata networks. The algorithm employs bitstate hashing with a perfect hash function, i.e. no collisions can occur. Two variations of this algorithm are discussed. Two examples are exercised to demonstrate the benefits of the new algorithm.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Balbo, G. Chiola, G. Franceschinis, and G. Molinar-Roet. On the efficient construction of the tangible reachability graph of generalized stochastic Petri nets. In Int. Work. Petri Nets and Performance Models. IEEE Computer Society, 1987.
A. Blakemore. The cost of eliminating vanishing markings from generalized stochastic Petri nets. In 3rd Int. Work. Petri Nets and Performance Models. IEEE Computer Society, 1989.
P. Buchholz. Numerical solution methods based on structured descriptions of Markovian models. In 5th Int. Conf. Modeling Techniques and Tools, 1991.
P. Buchholz. Markovian process algebra: Composition and equivalence. In 2nd Work. Process Algebras and Performance Modelling, 1994.
P. Buchholz. On a Markovian process algebra. Technical Report 500, Universität Dortmund, 1994.
S. Caselli, G. Conte, F. Bonardi, and M. Fontanesi. Experiences on SIMD massively parallel GSPN analysis. In Computer Performance Eval., Springer, 1994.
S. Caselli, G. Conte, and P. Marenzoni. Parallel state space exploration for GSPN models. In 16th int. Conf. Application and Theory of Petri Nets, Springer, 1995.
G. Chiola. Compiling techniques for the analysis of stochastic Petri nets. In 4th Int. Conf. on Modeling Techniques and Tools, Mallorca, 1989.
S. Christensen and L. Petrucci. Modular state space analysis of coloured Petri nets. In 16th int. Conf. Application and Theory of Petri Nets, Springer, 1995.
G. Ciardo and K.S. Trivedi. A decomposition approach for stochastic Petri net models. In 4th Int. Work. Petri Nets and Performance Models. IEEE Computer Society, 1991.
M. Davio. Kronecker products and shuffle algebra. IEEE Transactions on Computers, C-30(2):116–125, February 1981.
S. Donatelli. Superposed stochastic automata: a class of stochastic Petri nets with parallel solution and distributed state space. Performance Eval., 18:21–26, 1993.
S. Donatelli. Superposed generalized stochastic Petri nets: definition and efficient solution. In 15th int. Conf. Application and Theory of Petri nets, Springer, 1994.
P. Godefroid. Using partial orders to improve automatic verification methods. In 2nd int. Work. Computer Aided Verification, LNCS 531. Springer, 1990.
P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In 5th int. Conf. Computer Aided Verification, LNCS 697. Springer, 1993.
G.J. Holzmann. On limits and possibilities of automated protocol analysis. In 7th int. Work. Protocol Specification, Testing, and Verification. North-Holland, 1987.
G.J. Holzmann. An analysis of bitstate hashing. In 15th int. Symp Protocol Specification, Testing and Verification, IFIP. Chapman & Hall, 1995.
P. Kemper. Closing the gap between classical and tensor based iteration techniques (extended abstract). In Computations with Markov Chains. Kluwer, 1995.
P. Kemper. Numerical analysis of superposed GSPNs. In 6th Int. Work. Petri Nets and Performance Models. IEEE Computer Society Press, 1995.
B. Plateau and K. Atif. Stochastic automata network for modelling parallel systems. IEEE Trans, on Software Engineering, 17(10):1093–1108, 1991.
B. Plateau and J.M. Fourneau. A methodology for solving Markov models of parallel systems. Journal of Parallel and Distributed Computing, 12, 1991.
W.J. Stewart. Introduction to the numerical solution of Markov chains. Princeton University Press, 1994.
A. Valmari. Error detection by reduced reachability graph generation. In 9th Europ. Work. Application and Theory of Petri Nets, Venice, Italy, 1988.
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, LNCS 483. Springer, 1990.
P. Wolper and P. Godefroid. Partial order methods for temporal verification. In 4th int. Conf. Concurrency Theory, LNCS 715. Springer, 1993.
P. Wolper and D. Leroy. Reliable hashing without collision detection. In 5th int. Conf. Computer Aided Verification, Elounda, Greece, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kemper, P. (1996). Reachability analysis based on structured representations. 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_15
Download citation
DOI: https://doi.org/10.1007/3-540-61363-3_15
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