量化交替转换系统的模拟关系

Simulations for Quantitative Alternating Transition Systems

在形式化方法中,交替转换系统是一种重要的刻画开放系统的形式化模型。为了满足对开放系统量化验证的需要,提出量化交替转换系统模型,引入一种量化模拟关系来衡量系统上状态之间的近似关系,并研究了这种模拟关系的基本性质。研究结果表明,量化模拟关系是交替转换系统上的模拟关系的自然扩展形式。

Alternating transition systems are a general model for open systems. To satisfy the need of quantitative verification of open systems,in this paper, we present a quantitative version of alternating transition systems, called quantitative alternating transition systems （QATSs）. We then establish a quantitative simulation between states of QATSs to quantify to what extent one state is simulated by another,and discuss its some properties. The obtained results show that our simulation is a natural extension of traditional one.