On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets

In this paper we present efficient techniques for the generation of very large continuous-time Markov chains (CTMCs) specified as stochastic Petri nets (SPNs). In particular, we investigate how the storage efficiency of the reachability graph generation can be improved by using good state coding techniques and by using hashing tables instead of tree-based data structures. These techniques allow us to analyse SPNs with almost 55 million states on a single workstation. The size of the SPNs that can be handled is then further enlarged by using a cluster of workstations. With 16 workstations, connected via a 100 Mbps Ethernet, we can generate reachability graphs with over 400 million states in reasonable time. The presented techniques have been realised in a prototype tool (PARSECS) implemented in C++ using the libraries STL and MPICH. The SPNs to be input to PARSECS are specified using CSPL, known from the tool SPNP. In the paper we present our techniques and study their performance for a number of case studies. We also present comparisons with SPNP