Abstract
Supply chain [2, 6] is an important component of 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 develop Stochastic Merchandise Flow Model (SMF), a formal framework for modeling stochastic supply chains based on Extended Markov Decision Process (EMDP); second, we propose 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-checking-based approach by applying it to a variety of stochastic supply chain models.