摘要：進(jìn)程代數(shù)是刻畫并發(fā)與交互式反應(yīng)系統(tǒng)行為的重要模型之一,進(jìn)程間的(互)模擬關(guān)系及其公理化以及結(jié)構(gòu)化操作語(yǔ)義(structural operational semantics,SOS)理論是其重要的兩個(gè)研究方向。共變-異變模擬(covariant-contravariant simulation,CC-模擬)是(互)模擬關(guān)系概念的推廣,它對(duì)動(dòng)作進(jìn)行區(qū)分,表達(dá)了狀態(tài)的行為數(shù)目越多但并不一定越好的事實(shí)。行為關(guān)系的(前)同余性質(zhì)在支持其形式規(guī)范的模塊化構(gòu)建和公理系統(tǒng)的推理方面具有重要意義。(前)同余性的證明需要根據(jù)進(jìn)程代數(shù)語(yǔ)言中算子的SOS規(guī)則逐個(gè)驗(yàn)證。為了避免(前)同余性證明的重復(fù)勞動(dòng),學(xué)術(shù)界提出了多種類型的SOS規(guī)則的框架形式。ntyft/ntyxt規(guī)則形式是目前具有代表性的SOS規(guī)則框架形式之一。文中基于ntyft/ntyxt規(guī)則形式,提出了能滿足CC-模擬前同余性的最大ntyft/ntyxt子類CC-ntyft/ntyxt規(guī)則形式,并證明了CC-模擬相對(duì)CC-ntyft/ntyxt算子的前同余性。