In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 269-288. Springer-Verlag, June 1996.
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.