摘要：進(jìn)程的行為理論是進(jìn)程演算研究的核心內(nèi)容之一,其側(cè)重于討論進(jìn)程間的行為等價(jià)和模擬關(guān)系。共變-異變模擬(Covariant-Contravariant Simulation,CC-模擬)的概念是對經(jīng)典(互)模擬概念的推廣,它通過區(qū)分動(dòng)作類型,刻畫了規(guī)范與實(shí)現(xiàn)對系統(tǒng)主動(dòng)、被動(dòng)和通訊動(dòng)作在精化關(guān)系中的不同要求。行為關(guān)系的(前)同余性和公理刻畫是進(jìn)程演算代數(shù)特征的集中體現(xiàn),它們對規(guī)范及實(shí)現(xiàn)的分析和推理至關(guān)重要。一般而言,行為關(guān)系(前)同余性的證明和公理系統(tǒng)的構(gòu)造需要基于不同進(jìn)程演算系統(tǒng)的結(jié)構(gòu)化操作語義(Structural Operational Semantics,SOS)分別展開。為了避免這類研究工作中的重復(fù)勞動(dòng),學(xué)術(shù)界針對一般化SOS規(guī)則形式的元理論開展了研究,GSOS是其中被廣泛研究的規(guī)則形式之一。文中在考量了動(dòng)作類型的基礎(chǔ)上,基于CC-模擬對GSOS規(guī)則形式做出擴(kuò)充,提出了CC-GSOS規(guī)則類型,證明了CC-模擬相對于CC-GSOS算子具有前同余性,并給出了在這些算子下CC-模擬的可靠完備公理系統(tǒng)的一般性構(gòu)造方法。
注：因版權(quán)方要求，不能公開全文，如需全文，請咨詢雜志社
