摘要：进程代数是刻画并发与交互式反应系统行为的重要模型之一,进程间的(互)模拟关系及其公理化以及结构化操作语义(structural operational semantics,SOS)理论是其重要的两个研究方向。共变-异变模拟(covariant-contravariant simulation,CC-模拟)是(互)模拟关系概念的推广,它对动作进行区分,表达了状态的行为数目越多但并不一定越好的事实。行为关系的(前)同余性质在支持其形式规范的模块化构建和公理系统的推理方面具有重要意义。(前)同余性的证明需要根据进程代数语言中算子的SOS规则逐个验证。为了避免(前)同余性证明的重复劳动,学术界提出了多种类型的SOS规则的框架形式。ntyft/ntyxt规则形式是目前具有代表性的SOS规则框架形式之一。文中基于ntyft/ntyxt规则形式,提出了能满足CC-模拟前同余性的最大ntyft/ntyxt子类CC-ntyft/ntyxt规则形式,并证明了CC-模拟相对CC-ntyft/ntyxt算子的前同余性。