Abstract:

The stratification of bisimilarity is an important issue in the classical research on bisimilarity. It provides a theoretical basis for some checking algorithms of bisimilarity. We establish the stratification of (η,α)-bisimilarity in this paper.(η,α)-bisimilarity is a notion of approximate bisimilarity with discount factor. It is defined with a discounted setting, which means that the difference occurring in the far away future is not as important as the difference occurring in the near future, which will be revealed in the stratification established in this paper. Moreover, since (η,α)bisimilarity is not always an equivalence relation, the coarsest partition method used in classical checking algorithms of bisimilarity cannot be adopted to offer a checking algorithm of (η,α)bisimilarity.Based on the stratification of (η,α)-bisimilarity, we provide a checking algorithm of this bisimilarity.We also offer a simple example to illustrate how to apply (η,α)-bisimilarity and its checking algorithm to capture the satisfaction relation between implementations and specifications.

Key words: (η,α)-bisimilarity;stratification;checking algorithm;discount