技術領域

本發(fā)明屬于隨機系統(tǒng)性能與可靠性分析技術領域，涉及面向連續(xù)時間馬爾科夫鏈的狀態(tài)空間約簡技術。

背景技術

模型檢測是一種自動化程度非常高的有限狀態(tài)系統(tǒng)驗證技術，目前已經在計算機硬件、通信與安全協議、軟件可靠性的驗證方面獲得了較大的成功。傳統(tǒng)模型檢測技術關注的是系統(tǒng)行為的絕對正確性，如系統(tǒng)不能進入死鎖狀態(tài)。然而分布式算法，多媒體協議，容錯系統(tǒng)等往往關心某種量化屬性，如消息傳送失敗的概率不高于1%，在時間t內至多m個消息丟失的概率不高于0.8%，請求發(fā)送后在5到7個時間單元內得到響應的概率不低于70%等等。隨機模型檢測致力于解決這類屬性的自動化驗證問題。

在隨機模型檢測中一般使用概率計算樹邏輯PCTL和連續(xù)隨機邏輯CSL刻畫屬性，使用馬爾科夫過程建立系統(tǒng)模型，主要包括離散時間馬爾可夫鏈，馬爾科夫決策過程，連續(xù)時間馬爾科夫鏈等。每種模型都具有一定的特性，不同的特性決定了模型表達和分析的重點不一樣。與其它模型相比，連續(xù)時間馬爾科夫鏈的主要特性在于能刻畫連續(xù)時間和指數分布。這兩種特性使得連續(xù)時間馬爾科夫鏈的模型檢測近年來成為一種成功的定量分析技術。

連續(xù)時間馬爾科夫鏈的模型檢測技術主要關注于隨機系統(tǒng)的性能、可靠性等性質的定量分析。例如Ender?Yüksel通過利用連續(xù)時間馬爾科夫鏈為我國智能電網中的傳感網絡建立隨機模型，并計算出了長期運行中傳感節(jié)點失效的概率，以及更換傳感器中電池的最優(yōu)時間段。Shinji?Kikuchi對云計算系統(tǒng)中并發(fā)實時遷移操作的性能進行了分析，計算出了某個時間段內發(fā)送服務器上多于4個遷移操作的概率，以及某個時間段內接受服務器上超過3個遷移操作正在處理的概率。M.Kwiatkowska通過分別計算傳感器、執(zhí)行器、輸入輸出處理器、中心計算處理器引起系統(tǒng)關閉的概率，分析了嵌入式控制系統(tǒng)的可靠性。

連續(xù)時間馬爾科夫鏈的模型檢測技術在生物學領域也有著重要的應用。MartaZ.Kwiatkowska分析了成纖維細胞生長因子信號通路的健壯性，并給出了系統(tǒng)各種動態(tài)行為的量化度量，從而加深了對信號通路的理解。J.Heath對分裂素激活的蛋白激酶級聯反應系統(tǒng)中各個成分之間的交互進行了定量刻畫。這些成功的應用實例說明模型檢測連續(xù)時間馬爾科夫鏈是對馬爾科夫過程傳統(tǒng)分析技術的有力擴展與補充。

目前連續(xù)時間馬爾科夫鏈的模型檢測方法是一種全局檢測方法，即通過遍歷整個系統(tǒng)的全局空間完成屬性的分析，因此與傳統(tǒng)模型檢測一樣，狀態(tài)空間爆炸依舊是模型檢測連續(xù)時間馬爾科夫鏈實用化的主要瓶頸（這里狀態(tài)空間爆炸是指對于并發(fā)系統(tǒng)，其狀態(tài)的數目往往隨著并發(fā)分量的增加呈指數增長），約簡狀態(tài)空間對提高模型檢測連續(xù)時間馬爾科夫鏈技術的實用性至關重要。

限界模型檢測是一種有效的空間約簡方法，其基本思想是在有限的局部空間中逐步搜索屬性成立的證據或者失效的反例，從而達到約簡狀態(tài)空間的目的。連續(xù)時間以及指數分布是連續(xù)時間馬爾科夫鏈上的兩個主要特性，這兩種特性為應用限界檢測來約簡連續(xù)時間馬爾科夫鏈上的狀態(tài)空間帶來了新的重要的問題，如在有窮路徑約束下瞬態(tài)概率與穩(wěn)態(tài)概率的計算，不同的時間約束類型對限界滿足性的影響不同，以設置路徑長度的上限作為判斷算法終止的標準已經失效，必須設計新的標準等等。這些新問題說明將限界檢測方法應用于約簡連續(xù)時間馬爾科夫鏈是不平凡的，有必要對該方法進行全新的研究。

發(fā)明內容

本發(fā)明的目的在于提供一種面向連續(xù)時間馬爾科夫鏈的狀態(tài)空間約簡方法，以提高模型檢測連續(xù)時間馬爾科夫鏈在分析隨機系統(tǒng)性能與可靠性上的實用性，提高可處理系統(tǒng)的規(guī)模。

為了解決以上技術問題，本發(fā)明的采用的技術方案如下。

一種面向連續(xù)時間馬爾科夫鏈的狀態(tài)空間約簡方法，其特征在于包括以下步驟：

步驟一，在局部狀態(tài)空間上配置連續(xù)隨機邏輯中X，U，R，P，W算子的限界語義

令為連續(xù)時間馬爾科夫鏈。對任意的狀態(tài)s∈S和界k，φ∈CSL，滿足性關系s|＝_kφ遞歸配置如下：

·對任意的s∈S，s|＝_ktrue；

·s|＝_ka當且僅當a∈L(s)；

·當且僅當

·當且僅當s|＝_kφ，s|＝_kψ；

·當且僅當s|＝_kφ或者s|＝_kψ；

·s|＝_kP_～p[φ]當且僅當Prob^C(s,φ,k)～p；