Performance Evaluation on Uniform Interactive Markov Chains

The models we considered in this paper are uniformed nondeterminism interactive Markov chains (IMCs). To give the performance specification of IMCs, we first give an algorithm to compute the optimize path probability to reach a set of goal states within a given time bound on an IMC MD, which describing until operator. Using an action-based logic called aCSL the properties of interesting over the IMCs models are described. The correctness of our describing method is proved. It is an extension of performance evaluation pure continue-time Markov chains.