—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 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 mod...