保證計(jì)算機(jī)系統(tǒng)的正確性和可靠性是計(jì)算機(jī)研究和開(kāi)發(fā)人員的首要任務(wù)。模型檢測(cè)是保證計(jì)算機(jī)系統(tǒng)正確性和可靠性的有力手段。當(dāng)人們對(duì)復(fù)雜系統(tǒng)進(jìn)行建模和分析時(shí),往往需要考慮到事件發(fā)生的不確定性、發(fā)生事件的時(shí)限和完成事件所付出的代價(jià)等因素,實(shí)時(shí)隨機(jī)系統(tǒng)模型檢測(cè)就是研究這類(lèi)情況下的模型檢測(cè)問(wèn)題。實(shí)時(shí)隨機(jī)系統(tǒng)模型檢測(cè)是誕生于二十世紀(jì)九十年代的一個(gè)活躍的研究領(lǐng)域,目前已取得很多重要的理論研究成果,并取得廣泛的實(shí)際應(yīng)用。為驗(yàn)證實(shí)時(shí)隨機(jī)系統(tǒng)的行為是否滿足一定性質(zhì)的要求,可以采用模型檢測(cè)的方法。如果系統(tǒng)的行為不滿足性質(zhì)的要求,可生成相應(yīng)的反例。進(jìn)一步地,為控制含不確定性的系統(tǒng)的行為,可以根據(jù)系統(tǒng)的模型和性質(zhì)的要求,合成適當(dāng)?shù)目刂破?以控制系統(tǒng)的運(yùn)行。本文正是圍繞實(shí)時(shí)隨機(jī)系統(tǒng)的分析、診斷與控制,開(kāi)展了一定的研究。實(shí)時(shí)隨機(jī)系統(tǒng)的典型模型包括離散（連續(xù)）時(shí)間Markov鏈、離散（連續(xù)）時(shí)間Markov決策過(guò)程、概率時(shí)間自動(dòng)機(jī)。本文圍繞離散（連續(xù)）時(shí)間Markov決策過(guò)程、概率時(shí)間自動(dòng)機(jī)及其擴(kuò)展模型,開(kāi)展了如下研究:1、面向概率時(shí)間自動(dòng)機(jī)的兩個(gè)擴(kuò)展模型—代價(jià)概率時(shí)間自動(dòng)機(jī)和區(qū)間概率時(shí)間自動(dòng)機(jī),研究了模型檢測(cè)問(wèn)題:（1）... 

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

【文章頁(yè)數(shù)】：88 頁(yè)

【學(xué)位級(jí)別】：博士

【部分圖文】：

一個(gè)建模網(wǎng)絡(luò)協(xié)議的概率時(shí)間自動(dòng)機(jī)

使用連續(xù)時(shí)間 Markov 鏈表示一個(gè)數(shù)據(jù)傳輸系統(tǒng)某節(jié)點(diǎn)的工路徑 CTMC 中的一條無(wú)限路徑σ 是一個(gè)狀態(tài)和22...ts → ，其中對(duì)于 i ∈ ，is ∈ S，且i0t>∈ ，使CPath 描述 CTMC C 中路徑的集合。當(dāng)ks 為一個(gè)吸收狀條有限路徑。允許范圍。令 [ ]iσ i = s， ( , )iδ σ i ∈ I。用,0 1( ,..., , )k kC s I I s 區(qū)間為 Ii的有限路徑。以 Ω ( Path)表示包含各個(gè),0 ( ,..C s I 由一個(gè)初始分布α 在路徑上產(chǎn)生的概率度量記為Prα。地定義為[4]：0( s)= α，( ) ( , , 0 0,..., ', ')) Pr ( ( ,..., )) ( , ') ( k E s a E sk k k s I s C s I s P s s e eα = sup I'。（當(dāng)b = ∞且 λ > 0時(shí)，令 e0 λ ∞= ）率分為瞬態(tài)概率和穩(wěn)態(tài)概率兩種。瞬態(tài)概率是系統(tǒng)在給定在達(dá)到平衡時(shí)的概率。瞬態(tài)概率的定義可形式化地描述為'C C

' [ : 0]( , ')X rp r lυ υ ∧ = =。自動(dòng)機(jī)的語(yǔ)法定義和語(yǔ)義描述可見(jiàn)，一個(gè)代價(jià)概率概率分支擴(kuò)展，也可看作是概率時(shí)間自動(dòng)機(jī)的概率示為一個(gè)具有時(shí)鐘 x的 P2TA。其中，每個(gè)圓圈代表的代價(jià)變化速率和不變式，包含在圓圈中。從一個(gè)或單一的邊�；诟怕实倪�，包含若干概率分支。選上。每個(gè)邊上包含衛(wèi)士、代價(jià)和待復(fù)位時(shí)鐘變量。當(dāng)率為 1 時(shí)，也忽略不寫(xiě)。設(shè)自動(dòng)機(jī)的初始位置為 l0位于一個(gè)位置時(shí)，若滿足該位置的不變式條件，可代價(jià)也相應(yīng)增加。設(shè)停留時(shí)間為d ，代價(jià)變化速率上的衛(wèi)士時(shí)，自動(dòng)機(jī)從一個(gè)位置躍遷到下一個(gè)位置的增長(zhǎng)為h。

【參考文獻(xiàn)】：
期刊論文
[1]模型檢測(cè)基于概率時(shí)間自動(dòng)機(jī)的反例產(chǎn)生研究[J]. 張君華,黃志球,曹子寧.  計(jì)算機(jī)研究與發(fā)展. 2008(10)
[2]基于Horn邏輯擴(kuò)展模型的安全協(xié)議反例的自動(dòng)構(gòu)造[J]. 周倜,李夢(mèng)君,李舟軍,陳火旺.  計(jì)算機(jī)研究與發(fā)展. 2007(09)



本文編號(hào)：3562658