An approach of model checking time or space performance

It has been a research focus that the performance analysis of complex systems such as network protocols which include nondeterministic choices. Besides time, space aspect is also considered during the process of performance evaluation. By model checking, we can verify whether time or space performance meets expected constraints. The authors adopt CTMRP (Continuous-Time Markov Reward Process) as the verification model since it can depict nondeterminism intuitively. The temporal logic CSRL (Continuous Stochastic Reward Logic) is extended by replacing path operators with regular expressions in order to express more comprehensive time or spatial properties which are based on states or paths. For deterministic schedulers, a duality result of constrained reachability probabilities between time and space is proposed, and its correctness is proved based on the existing work. Based on the theoretical consequences, the verification of space performance is reduced to the corresponding analysis of time reachability. The model checking algorithm and a new approach for the performance evaluation of complex systems are given.