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

步驟一，在將路徑長(zhǎng)度約束在有限長(zhǎng)度的情況下配置連續(xù)隨機(jī)邏輯中X，U，R，P，W五個(gè)算子的限界語(yǔ)義；X為表示“下一個(gè)時(shí)刻”的時(shí)態(tài)算子，U為表示“一直到”的時(shí)態(tài)算子，R為表示“釋放”的時(shí)態(tài)算子，P為概率度量算子，W為穩(wěn)態(tài)算子；

步驟二，在將路徑長(zhǎng)度約束在有限長(zhǎng)度的情況下計(jì)算局部空間上狀態(tài)之間的k界瞬態(tài)概率，這里k是自然數(shù)；

步驟三，在將路徑長(zhǎng)度約束在有限長(zhǎng)度的情況下利用k界瞬態(tài)概率計(jì)算X，U，R，P，W算子對(duì)應(yīng)的概率度量，并依據(jù)計(jì)算結(jié)果判定X，U，R，P，W算子的概率度量是否滿足限界語(yǔ)義。

2.一種面向連續(xù)時(shí)間馬爾科夫鏈的狀態(tài)空間約簡(jiǎn)方法，其特征在于所述步驟一進(jìn)一步具體為：

步驟1,配置P算子的限界語(yǔ)義：s|＝_kP_～p[φ]當(dāng)且僅當(dāng)Prob^C(s,φ,k)～p；

步驟2,配置W算子的限界語(yǔ)義：s|＝_kW_～p[φ]當(dāng)且僅當(dāng)

步驟3,計(jì)算概率度量Prob^C(s,φ,k)：Prob^C(s,φ,k)＝Pr_s{ω∈Path^C(s)|ω|＝_kφ}，且對(duì)任意的路徑ω∈Path^C(s)：

ω|＝_kXφ當(dāng)且僅當(dāng)k≥1，且ω(1)|＝_kφ；

ω|＝_kφU^Iψ當(dāng)且僅當(dāng)

ω|＝_kφR^Iψ當(dāng)且僅當(dāng)或者

各參數(shù)的解釋如下：

φ、ψ是連續(xù)隨機(jī)邏輯公式；

s是連續(xù)時(shí)間馬爾科夫鏈中的狀態(tài)；

|＝_k是在界k的約束下?tīng)顟B(tài)滿足連續(xù)隨機(jī)邏輯公式；

～p表示p是[0,1]上的實(shí)數(shù)，～∈{＜,≤,＞,≥}；

Prob^C(s,φ,k)表示連續(xù)時(shí)間馬爾科夫鏈C中在路徑長(zhǎng)度為k的約束下?tīng)顟B(tài)s滿足連續(xù)隨機(jī)邏輯公式φ的概率；

表示連續(xù)時(shí)間馬爾科夫鏈C中在時(shí)刻t系統(tǒng)處于狀態(tài)s的k界瞬態(tài)概率；

Pr_s{ω∈Path^C(s)|ω|＝_kφ}表示從狀態(tài)s出發(fā)所有長(zhǎng)度為k且滿足φ的路徑集合的概率；

ω表示一個(gè)非空序列s₀t₀s₁t₁s₂...，其中對(duì)任意的i≥0，R(s_i,s_i+1)＞0，t_i為非負(fù)實(shí)數(shù)；

ω(i)表示序列ω上的第i個(gè)狀態(tài)；

Path^C(s)表示連續(xù)時(shí)間馬爾科夫鏈C上從狀態(tài)s出發(fā)的路徑的集合，包括有窮路徑和無(wú)窮路徑；

I為實(shí)數(shù)上的區(qū)間；

ω@t表示對(duì)于無(wú)窮路徑ω在時(shí)刻t系統(tǒng)所處的狀態(tài)，即ω(j)，j是使得成立的最小的整數(shù)；

position(ω,t)表示對(duì)于路徑ω＝s₀t₀s₁t₁s₂...，引入記號(hào)position(ω,t)表示使得成立的最小的整數(shù)j；表示“存在一個(gè)”；表示表示“任意的”。