LTL概率模型檢驗(yàn)優(yōu)化技術(shù)的研究.pdf

1、概率模型檢驗(yàn)是一種針對(duì)概率模型的形式化驗(yàn)證技術(shù)，與傳統(tǒng)的非概率模型檢驗(yàn)相比，概率模型檢驗(yàn)不僅能對(duì)系統(tǒng)進(jìn)行定性的檢驗(yàn)，即判斷系統(tǒng)是否滿足某個(gè)給定的性質(zhì)，而且還能定量的對(duì)概率系統(tǒng)，或者具有概率行為的系統(tǒng)進(jìn)行檢驗(yàn)，即模型在哪個(gè)概率區(qū)間滿足給出的性質(zhì)。概率模型檢驗(yàn)中，通常用線性時(shí)序邏輯(Linear Temporal Logic，LTL)和計(jì)算樹邏輯(Computational Tree Logic，CTL)來描述系統(tǒng)性質(zhì)。雖然LTL與CTL表

2、達(dá)能力有交集，但是如公平性性質(zhì)這樣重要的性質(zhì)只能用LTL來表示。然而，相比于CTL，當(dāng)前LTL概率模型檢驗(yàn)算法的復(fù)雜度非常高，驗(yàn)證效率很低，因此目前已有的概率模型工具如MRMC和PRISM均不支持對(duì)LTL性質(zhì)的驗(yàn)證。
　　針對(duì)這個(gè)問題，本文提出了一種基于概率保持的公式化簡(jiǎn)技術(shù)。該優(yōu)化技術(shù)通過縮短待驗(yàn)證公式的長(zhǎng)度來減小算法執(zhí)行的時(shí)空開銷，從而提高算法的執(zhí)行效率，在一定程度上緩解了LTL概率模型檢驗(yàn)算法復(fù)雜度高的難題。
　　以上