n-精化与 n-互模拟之间相关问题的研究-《计算机技术与发展》

文章信息/Info

作者:: 施晓静1 ; 张晋津2; 1. 南京航空航天大学计算机科学与技术学院,江苏南京 210016;
2. 南京审计学院计算机科学与技术系,江苏南京 211815

Author(s):: SHI Xiao-jing 1 ; ZHANG Jin-jin 2; 1. School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China；
2. Department of Computer Science and Technology,Nanjing Audit University,Nanjing 211815,China

Keywords:: n-refinement; n-bisimualtion; translation function; relativization

摘要:: n-精化关系在计算机科学领域中发挥着重要作用。在理论计算机科学中,学者们常用互模拟来刻画状态转换系统(例如,实时控制系统)之间的行为关系,当两个系统之间存在互模拟等价关系时,从某种意义上来说,一个系统的行为可以模拟另一个系统,反之亦然。但是互模拟关系并不能使得在模型检测时所需检测状态空间得到明显的缩减,因此引入了精化关系。精化与互模拟的区别在于,其对向前条件没有限制,如果精化关系满足向前条件,那么该精化关系也是互模拟关系。在刻画系统状态之间精化关系是否在有限的可达关系上成立这个问题时,需要将精化扩展到 n-精化关系上,从而提出 n-精化的概念,进一步地,探究 n-精化关系与 n-互模拟关系的联系；提出与标准相对化不同的 a-相对化的概念,并研究其与标准相对化之间的区别与联系；在这些研究基础上,将 n-精化模态逻辑语言翻译成 n-互模拟量化语言。

Abstract:: The notion of n-refinement plays an important role in computer science. In the area of theoretical computer science,researchers often use bisimulations to model the action of different state transition systems,such as real-time control system. While there exits bisimulation equivalence relation of the two systems,in a sense,the behavior of one of these two systems can simulate the other system，s behavior,and vice versa. However,this relation does not often make the state space significantly reduced,so the notion of the refinement relationship was introduced. The difference between refinement and bisimulation is that there is no restriction in the forth condition,but when refinement satisfies the forth condition,then we get the bisimulation back. To characterize the problem that whether the refinement between the state of the system exists in a limited accessible relation,we need to introduce the n-refinement. So in this paper,the concept of n-refinement is given based on the refinement,and we could further explore the relationship between n-refinement and n-bisimulation.The notion of a-relativization which is different from the standard version is proposed,and the relationship between them are researched.Then we present the translation function from n-refinement modal logic language into n-bisimulation quantification language.