Li Tan and Shenghan Xu. In Proceedings of the 2011 annual meeting of Production and Operation Management Society. Reno, NV. April, 2011.

Probabilistic model checking is an automated verification technique that provides a “push-button” approach for algorithmatically analyzing probabilistic systems. Probabilistic model checking has been successfully used for analyzing the performance of a variety of dynamic systems in Computer Science and other fields such as bioinformatics. In this research we will apply probabilistic model checking to the performance analysis of probabilistic supply chains. Particularly we formulate the cost structure of supply chains using reward mechanism in probabilistic model checking. As an application, we will use probabilistic model checking to analyze the impact of different risk factors on the holding of safety stock. We will show that a probabilistic model checker such as PRISM provides an efficient decision procedure for safety stock.