A Language for Performance Evaluation Based on the Combination of CTRML and MMTD and Its Algorithm

Safety-critical systems are becoming more common around us, how to conduct performance evaluation becomes an important practical concern. Performance evaluation means to describe, analyze, and optimize the dynamic, time-dependent behavior of systems. Traditional temporal logics, even probabilistic temporal logics are expressive enough, but they are limited to producing only true or false responses, as they are still logics. Meanwhile, the probabilistic operator can produce only true or false responses, without any other information, like the medium truth degree of the property. To overcome this problem, a novel language for performance evaluation was proposed, which absorbs the advantages of the existing formal languages and uses the distance ratio function of “Measure of Medium Truth Degree (MMTD)” to quantify the additional information, which we called fuzzy information. In addition, the existing approximate probabilistic bisimulation relations, which do not take the case of convex combination transitions into account, are deficient. To tackle this issue, a new approximate probabilistic bisimulation relation was put forward, which forms the basis for the novel language, especially for the probabilistic operator. The performance evaluation algorithm and properties related to the new language are given. The expressive ability of the novel language for performance evaluation was demonstrated by a case study.