一種高階進(jìn)程代數(shù)的弱互模擬研究.pdf

1、進(jìn)程代數(shù)作為描述和分析并發(fā)與分布式系統(tǒng)的重要工具之一，是并發(fā)理論的主流研究方向?；ツM是進(jìn)程代數(shù)的核心概念之一，用來刻畫進(jìn)程之間的等價(jià)關(guān)系，其中描述觀察等效的弱互模擬是最為重要的互模擬之一，其性質(zhì)往往比較難以研究。 高階進(jìn)程代數(shù)在描述一些系統(tǒng)的時(shí)候比較直觀，很有優(yōu)勢(shì)，受到越來越多的關(guān)注，但高階進(jìn)程代數(shù)的性質(zhì)難以刻畫。本文研究的高階演算一直沒有一個(gè)很自然且相對(duì)簡(jiǎn)單的建立在帶標(biāo)記語義系統(tǒng)之上的等價(jià)關(guān)系，不是給定的互模擬性質(zhì)太強(qiáng)，就是

2、給出的互模擬證明很繁瑣。有學(xué)者用環(huán)境帶標(biāo)記的轉(zhuǎn)換語義來刻畫高階進(jìn)程代數(shù)，給出的互模擬形式相對(duì)簡(jiǎn)潔。 本文研究了建立在環(huán)境帶標(biāo)記的轉(zhuǎn)換基礎(chǔ)之上的受限的高階演算的弱互模擬，證明了弱互模擬的代數(shù)性質(zhì)和同余性質(zhì)。 近來，人們也越來越多地用規(guī)約語義描述進(jìn)程代數(shù)，因?yàn)橐?guī)約語義簡(jiǎn)潔且能給出一個(gè)滿意的數(shù)學(xué)分析。我們介紹了一個(gè)規(guī)約系統(tǒng)，基于它證明了其與上面給出的環(huán)境帶標(biāo)記的語義在弱互模擬的情況下是有等價(jià)關(guān)系的，即兩個(gè)進(jìn)程是弱互模擬的當(dāng)且僅