Bisimulation equivalence and logical preservation for green evaluation model

In green computing, the study of green evaluation approaches is an important area. Their main task is to validate whether the consumed time or spatial resources fall into specified bounds while the considered system running correctly. One can employ model checking, which is automatic, complete and effective, as a new green evaluation approach, but the emergence of state space explosion may result in that it is not available or ineffective when green evaluating. In this paper we model the considered systems as stochastic processes and the evaluation properties, which allowed for behavioral correctness and time or spatial resources constraints, are expressed by temporal logic. We define the bisimulation equivalence relation, which allowed for nondeterminacy, the syntax of bisimulation quotient and the policy of quotient model, and compare the quotient behavior with the original one. We also prove that the bisimulation equivalence relation preserve evaluation result. Thus, bisimulation equivalence can be viewed as a feasible states reduction approach, and provides theoretical foundation in model-based green evaluation approaches.