GSOS算子下共變G異變模擬的公理刻畫

摘要：進程的行為理論是進程演算研究的核心內容之一,其側重于討論進程間的行為等價和模擬關系。共變-異變模擬(Covariant-Contravariant Simulation,CC-模擬)的概念是對經典(互)模擬概念的推廣,它通過區分動作類型,刻畫了規范與實現對系統主動、被動和通訊動作在精化關系中的不同要求。行為關系的(前)同余性和公理刻畫是進程演算代數特征的集中體現,它們對規范及實現的分析和推理至關重要。一般而言,行為關系(前)同余性的證明和公理系統的構造需要基于不同進程演算系統的結構化操作語義(Structural Operational Semantics,SOS)分別展開。為了避免這類研究工作中的重復勞動,學術界針對一般化SOS規則形式的元理論開展了研究,GSOS是其中被廣泛研究的規則形式之一。文中在考量了動作類型的基礎上,基于CC-模擬對GSOS規則形式做出擴充,提出了CC-GSOS規則類型,證明了CC-模擬相對于CC-GSOS算子具有前同余性,并給出了在這些算子下CC-模擬的可靠完備公理系統的一般性構造方法。