Sound criteria for partial order reduction for probabilistic concurrent systems have been presented in the literature. Their realization relies on a depth-first search-based approachfor generating the reduced model. The drawback of this dynamicapproach is that it can hardly be combined with other techniquesto tackle the state explosion problem, e.g., symbolic probabilisticmodel checking with multi-terminal variants of binary decisiondiagrams. Following the approach presented by Kurshan et al. for non-probabilistic systems, we study partial order reductiontechniques for probabilistic concurrent systems that can berealized by a static analysis. The idea is to inject the reductioncriteria into the control flow graphs of the processes of the systemto be analyzed. We provide the theoretical foundations of staticpartial order reduction for probabilistic concurrent systems andpresent algorithms to realize them. Finally, we report on someexperimental results.
展开▼
