This talk addresses efficient techniques for the generation of very
large continuous-time Markov chains (CTMCs) specified as stochastic
Petri nets (SPNs). In particular, it is investigated how the storage
efficiency of the reachability graph generation can be improved by using
clever state coding techniques and by using hashing tables instead of
tree-based data structures. These techniques already allow us to analyse
SPNs with almost 55 million states on a single workstation. The size of
the SPNs that can be handled by these techniques is then further
enlarged by using a cluster of workstations. With a dozen work-stations,
connected via an ordinary Ethernet, reachability graphs with over 110
million states can be generated in reasonable time.
The techniques presented form the basis for model-based performance
evaluation studies and for model-checking algorithms.