In: Brinksma, E.; Hermanns, H.; Katoen, J.P.: LNCS 2090: Lectures on Formal Methods and Performance Analysis, pages 344-374. Springer-Verlag, 2001.
Abstract: Both the logic and the stochastic analysis of discrete-state systems are hindered by the combinatorial growth of the state space underlying a high-level model. In this work, we consider two orthogonal approaches to cope with this ``state-space explosion''. Distributed algorithms that make use of the processors and memory overall available on a network of N workstations can manage models with state spaces approximately N times larger than what is possible on a single workstation. A second approach, constituting a fundamental paradigm shift, is instead based on decision diagrams and related implicit data structures that efficiently encode the state space or the transition rate matrix of a model, provided that it has some structure to guide its decomposition; with these implicit methods, enormous sets can be managed efficiently, but the numerical solution of the stochastic model, if desired, is still a bottleneck, as it requires vectors of the size of the state space.