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

1、保證計算機系統(tǒng)的正確性和可靠性是計算機研究和開發(fā)人員的首要任務。模型檢測是保證計算機系統(tǒng)正確性和可靠性的有力手段。當人們對復雜系統(tǒng)進行建模和分析時，往往需要考慮到事件發(fā)生的不確定性、發(fā)生事件的時限和完成事件所付出的代價等因素，實時隨機系統(tǒng)模型檢測就是研究這類情況下的模型檢測問題。
　　 實時隨機系統(tǒng)模型檢測是誕生于二十世紀九十年代的一個活躍的研究領域，目前已取得很多重要的理論研究成果，并取得廣泛的實際應用。為驗證實時隨機系統(tǒng)的行

2、為是否滿足一定性質的要求，可以采用模型檢測的方法。如果系統(tǒng)的行為不滿足性質的要求，可生成相應的反例。進一步地，為控制含不確定性的系統(tǒng)的行為，可以根據(jù)系統(tǒng)的模型和性質的要求，合成適當?shù)目刂破?，以控制系統(tǒng)的運行.本文正是圍繞實時隨機系統(tǒng)的分析、診斷與控制，開展了一定的研究。實時隨機系統(tǒng)的典型模型包括離散(連續(xù))時間Markov鏈、離散(連續(xù))時間Markov決策過程、概率時間自動機。本文圍繞離散(連續(xù))時間Markov決策過程、概率時間自動

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

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

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