進(jìn)程代數(shù)與時(shí)序邏輯是并發(fā)理論中應(yīng)用最為廣泛的兩類規(guī)范系統(tǒng),其中進(jìn)程代數(shù)支持組合式的規(guī)范,而時(shí)序邏輯便于描述與驗(yàn)證系統(tǒng)的抽象性質(zhì)。近來,Gerald Luttgen等人將二者進(jìn)行結(jié)合,提出了邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)以及該系統(tǒng)下進(jìn)程項(xiàng)之間的精化關(guān)系——LLTS預(yù)備模擬關(guān)系。邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)將操作式與邏輯式的規(guī)范結(jié)合到了統(tǒng)一的框架中,在通常的標(biāo)記轉(zhuǎn)換系統(tǒng)的基礎(chǔ)上引入了進(jìn)程之間的合取,并以協(xié)調(diào)性謂詞標(biāo)記由合取所產(chǎn)生的不協(xié)調(diào)進(jìn)程,因而在支持組合式推理的同時(shí)還具有較強(qiáng)的表達(dá)能力。本文在充分考慮LLTS預(yù)備模擬相對于協(xié)調(diào)性謂詞以及發(fā)散敏感的特性基礎(chǔ)上,給出了判定不同邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)之間是否具有LLTS預(yù)備模擬關(guān)系的算法,主要工作包括如下方面:1.引入劃分對及其穩(wěn)定性的定義,證明穩(wěn)定劃分對與LLTS預(yù)備模擬關(guān)系之間的等價(jià)性�；谠摰葍r(jià)性,將判定不同邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)之間LLTS預(yù)備模擬關(guān)系的問題轉(zhuǎn)化為求解“最粗劃分”問題,給出求解最粗劃分的算子?,并證明其正確性。2.從更加一般化的角度看待LLTS預(yù)備模擬關(guān)系,提出與LLTS預(yù)備模擬關(guān)系等價(jià)的泛化預(yù)備模擬的定義,并證明了這一等價(jià)性。進(jìn)而基于此定義,提出相應(yīng)的劃分... 

【文章來源】：南京航空航天大學(xué)江蘇省 211工程院校

【文章頁數(shù)】：67 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
注釋表
縮略詞
第一章 緒論
    1.1 引言
    1.2 混成系統(tǒng)規(guī)范與邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)
    1.3 進(jìn)程間精化關(guān)系的判定
    1.4 本文的主要研究工作
第二章 基本概念與定義
    2.1 邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)
    2.2 LLTS上的邏輯構(gòu)造
    2.3 協(xié)調(diào)性謂詞的直觀
    2.4 LLTS下的預(yù)備模擬
第三章 LLTS下的穩(wěn)定劃分對
    3.1 劃分對
    3.2 reduct與expand函數(shù)的性質(zhì)
    3.3 劃分對的穩(wěn)定性
    3.4 本章小結(jié)
第四章 一般化最粗劃分問題及其求解
    4.1 一般化最粗劃分問題
    4.2 一般化最粗劃分的求解
    4.3 例子
    4.4 本章小結(jié)
第五章 LLTS預(yù)備模擬的判定算法
    5.1 LLTS泛化預(yù)備模擬
    5.2 劃分對的泛化穩(wěn)定性
    5.3 ERS算法
    5.4 算法復(fù)雜度
    5.5 例子
    5.6 本章小結(jié)
第六章 總結(jié)與展望
    6.1 全文總結(jié)
    6.2 進(jìn)一步的工作
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文



本文編號(hào)：3117332