Model Checking (k, d)-Markov Chain with ipLTL

摘要

In this paper a hierarchical Markov model is proposed for the temporal analysis of periodic stochastic systems. For analyzing the system behavior, an interval linear temporal logic, ipLTL, is presented, which is an LTL with linear inequalities on the probability mass functions (pmfs) as an atomic proposition. We prove that the proposed model converges to a steady state which enables us to develop an algorithm to determine the bound of the system execution time and check the specification written in ipLTL. Some properties of the manufacturing systems are analyzed and verified to illustrate the efficiency of our methods.