(η,α)-互模拟的分层及判定算法  

Stratification and checking algorithm of (η,α)-bisimilarity

作　　者：张晋津 张严[2] 朱朝晖[2] 

机构地区：[1]南京审计学院工学院,江苏南京211815 [2]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机工程与科学》2015年第3期547-552,共6页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60973045;11426136);江苏省高校自然科学基金资助项目(13KJB520012)

摘　　要：分层刻画是传统的互模拟概念研究中的一个重要内容,它为一些互模拟判定算法提供了理论基石。(η,α)-互模拟是一种带折扣的近似互模拟概念,其定义蕴涵着一种折扣思想:在比较系统差异时,越晚出现的差异越不重要。为(η,α)-互模拟建立分层刻画,将清晰地揭示这种折扣思想。此外,由于(η,α)-互模拟一般不是等价关系,所以传统的互模拟判定算法中常用的最粗划分方法不适用于(η,α)-互模拟的判定,基于(η,α)-互模拟的分层刻画给出一种该互模拟的判定算法。还提供一个简单的例子用于说明(η,α)-互模拟及其判定算法在描述实现与规范之间关系时的应用。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.

关 键 词：(η α)-互模拟 分层 判定算法 折扣 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]