Li Tan and Shenghan Xu. In the proceedings of the IEEE International Conference on Information Reuse and Integration (IRI'08). Las Vegas, NV, 2008.
Supply chain is an important componentof business operations. Understanding its stochastic behaviors is the key to risk analysis and performance evaluation in supply chain design and management.We propose a novel computational framework for modeling and analyzing the stochastic behaviors of a supply chain. The framework is based on probabilistic model checking, a formal verification technique for analyzing stochastic systems. Our approach is two-fold: first, we developed Stochastic Supply Chain Model (SMF), a formal framework for modeling stochastic supply chains based on Extended Markov Decision Process (EMDP); second, we proposed a model-checking-based formal technique to automate the analysis of a stochastic supply chain. Our model-checking-based approach leverages benefits of recent advances in symbolic probabilistic model checking to improve the efficiency and scalability of decision procedures. Using the temporal logic PCTL [1] and the symbolic probabilistic model checker PRISM [4], we are able to express and check complicate temporal and stochastic properties on supply chains. Finally, we demonstrate the capability of our model-checkingbased approach by testing it on a variety of stochastic supply chain models.