實(shí)時(shí)隨機(jī)系統(tǒng)的分析診斷與控制研究.pdf

1、保證計(jì)算機(jī)系統(tǒng)的正確性和可靠性是計(jì)算機(jī)研究和開發(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è)就是研究這類情況下的模型檢測(cè)問題。
　　 實(shí)時(shí)隨機(jī)系統(tǒng)模型檢測(cè)是誕生于二十世紀(jì)九十年代的一個(gè)活躍的研究領(lǐng)域，目前已取得很多重要的理論研究成果，并取得廣泛的實(shí)際應(yīng)用。為驗(yàn)證實(shí)時(shí)隨機(jī)系統(tǒng)的行

2、為是否滿足一定性質(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)的分析、診斷與控制，開展了一定的研究。實(shí)時(shí)隨機(jī)系統(tǒng)的典型模型包括離散(連續(xù))時(shí)間Markov鏈、離散(連續(xù))時(shí)間Markov決策過程、概率時(shí)間自動(dòng)機(jī)。本文圍繞離散(連續(xù))時(shí)間Markov決策過程、概率時(shí)間自動(dòng)

3、機(jī)及其擴(kuò)展模型，開展了如下研究：
　　 1、面向概率時(shí)間自動(dòng)機(jī)的兩個(gè)擴(kuò)展模型-代價(jià)概率時(shí)間自動(dòng)機(jī)和區(qū)間概率時(shí)間自動(dòng)機(jī)，研究了模型檢測(cè)問題：
　　 (1)以代價(jià)概率時(shí)間自動(dòng)機(jī)模型來描述系統(tǒng)，研究在一定概率下限條件下的最優(yōu)成本求解問題。將該模型擴(kuò)展為多代價(jià)概率時(shí)間自動(dòng)機(jī)，研究在一定概率下限和輔助成本上限約束條件下的主成本最小值的求解問題。針對(duì)每個(gè)問題，給出了求解算法和驗(yàn)證的實(shí)例。
　　 (2)提出了區(qū)間概率時(shí)間自動(dòng)機(jī)

4、模型，來描述離散遷移概率為區(qū)間值的實(shí)時(shí)隨機(jī)系統(tǒng)，并研究了區(qū)間概率時(shí)間自動(dòng)機(jī)的模型檢測(cè)問題。其核心問題是該模型上的最大概率計(jì)算問題。通過基于zone的反向?qū)挾葍?yōu)先搜索算法，得到寬松區(qū)間Markov決策過程。由于問題的等價(jià)性，將區(qū)間概率時(shí)間自動(dòng)機(jī)上的最大概率計(jì)算問題轉(zhuǎn)換為后者的最大概率計(jì)算問題。給出了寬松區(qū)間Markov決策過程上最大概率的計(jì)算方法。
　　 2、面向概率時(shí)間自動(dòng)機(jī)和連續(xù)時(shí)間Markov決策過程，研究了模型檢測(cè)時(shí)的反例

5、生成問題：
　　 (1)研究了模型檢測(cè)概率時(shí)間自動(dòng)機(jī)的反例生成問題。給出了模型檢測(cè)概率時(shí)間自動(dòng)機(jī)的反例的定義，給出了快速計(jì)算該反例的步驟和算法。在深入分析上述方法的基礎(chǔ)上，給出了計(jì)算該反例的精化算法。
　　 (2)研究了連續(xù)時(shí)間Markov決策過程上可達(dá)性的反例生成問題。在掌握連續(xù)時(shí)間Markov決策過程上的可達(dá)性驗(yàn)證算法的基礎(chǔ)上，給出了連續(xù)時(shí)間Markov決策過程上可達(dá)性的反例的概念，并給出了高效地計(jì)算該反例的步驟和算