基于Institution理論的結(jié)構(gòu)化轉(zhuǎn)換系統(tǒng)的研究.pdf

1、轉(zhuǎn)換系統(tǒng)作為經(jīng)典的形式化模型，被廣泛用于描述并發(fā)系統(tǒng)的行為。然而，在經(jīng)典的轉(zhuǎn)換系統(tǒng)中，標(biāo)記自身所包含的結(jié)構(gòu)性質(zhì)并未被考慮，當(dāng)考察附有特定要求的并發(fā)系統(tǒng)時(shí)，通常需要一些更具表達(dá)能力的轉(zhuǎn)換系統(tǒng)作為其形式化模型。針對(duì)一些特定領(lǐng)域或特定問題，學(xué)術(shù)界提出了各種標(biāo)記上帶有定量信息的轉(zhuǎn)換系統(tǒng)。
　　本文在帶定量信息的轉(zhuǎn)換系統(tǒng)的一個(gè)較一般框架（即，結(jié)構(gòu)化標(biāo)記轉(zhuǎn)換系統(tǒng)）下，從Institution理論的觀點(diǎn)出發(fā)，對(duì)結(jié)構(gòu)化部分互模擬、結(jié)構(gòu)化共變-逆變

2、模擬與結(jié)構(gòu)化模態(tài)精化三類關(guān)系及其內(nèi)在聯(lián)系展開研究，主要工作包括如下方面：
　　（1）引入了結(jié)構(gòu)化標(biāo)記轉(zhuǎn)換系統(tǒng)，提出結(jié)構(gòu)化部分互模擬和結(jié)構(gòu)化共變-逆變模擬，并分別采用模態(tài)邏輯語言LB和LCC建立了它們的邏輯刻畫。
　?。?）證明了結(jié)構(gòu)化標(biāo)記轉(zhuǎn)換系統(tǒng)以結(jié)構(gòu)化部分互模擬、結(jié)構(gòu)化共變-逆變模擬為模型態(tài)射在模態(tài)邏輯語言LB、LCC下分別構(gòu)成Institution結(jié)構(gòu)（記作I pb、I cc）；類似地，結(jié)構(gòu)化模態(tài)轉(zhuǎn)換系統(tǒng)以結(jié)構(gòu)化模態(tài)精化