加權(quán)遷移系統(tǒng)線性時(shí)間屬性及其安全性檢測(cè)

1、加權(quán)遷移系統(tǒng)線性時(shí)間屬性及其安全性檢測(cè)針對(duì)加權(quán)遷移系統(tǒng)，提出了線性時(shí)間屬性及其安全性檢測(cè)。 首先定義了半環(huán) K 上的加權(quán)遷移系統(tǒng)， 提出了加權(quán)線性時(shí)間屬性 概念，并根據(jù)權(quán)重函數(shù)確定加權(quán)線性時(shí)間屬性的上確界、 下確界 和閉包； 接著給出了幾種常見(jiàn)的加權(quán)線性時(shí)間屬性并且討論了 它們的關(guān)系； 然后重點(diǎn)研究了加權(quán)安全性，通過(guò)加權(quán)自動(dòng)機(jī)和 閉包給出了加權(quán)正則安全性； 最后基于加權(quán)有窮自動(dòng)機(jī)，建立 了加權(quán)正則安全性的檢測(cè)方法。檢測(cè)過(guò)程結(jié)合半環(huán)和形式冪級(jí) 數(shù)，構(gòu)造了加權(quán)遷移系統(tǒng)和加權(quán)有窮自動(dòng)機(jī)的乘積系統(tǒng)， 將加權(quán) 安全性檢測(cè)問(wèn)題轉(zhuǎn)化為驗(yàn)證乘積系統(tǒng)的不變性， 給出了加權(quán)正則 安全性檢測(cè)的算法和復(fù)雜度。 實(shí)例結(jié)

2、果表明， 所提的方法能夠?qū)?加權(quán)遷移系統(tǒng)的安全性進(jìn)行檢測(cè)。0 引言模型檢測(cè)是一種自動(dòng)驗(yàn)證技術(shù)， 在建立待測(cè)系統(tǒng)的有限狀態(tài) 模型基礎(chǔ)上， 通過(guò)顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來(lái)驗(yàn)證系統(tǒng)的 屬性，并且在不滿足屬性時(shí)提供反例路徑 1 。模型檢測(cè)的基本 思想是用狀態(tài)遷移系統(tǒng)表示待測(cè)系統(tǒng)的行為， 常用線性時(shí)序邏輯 (Linear Time Logic ，LTL )或計(jì)算樹(shù)邏輯 (Computational Tree Logic , CTL)的公式來(lái)刻畫(huà)系統(tǒng)的屬性，比如安全性、活性、 不變性。系統(tǒng)是否滿足所給定的屬性就等價(jià)于驗(yàn)證狀態(tài)遷移系統(tǒng) 是否是對(duì)應(yīng)公式的一個(gè)模型。 對(duì)于有窮狀態(tài)的系統(tǒng)來(lái)說(shuō)， 該問(wèn)題 是可判

3、定的，它等價(jià)于求一個(gè)有窮自動(dòng)機(jī)所滿足的屬性狀態(tài)集 合。模型檢測(cè)研究已被大量應(yīng)用于計(jì)算機(jī)硬件、通信協(xié)議、安全 認(rèn)證等分析中。目前，學(xué)者們已經(jīng)研究了大量不同類(lèi)型的模型檢測(cè)技術(shù)。 主 要研究對(duì)象是一類(lèi)系統(tǒng)屬性， 它們使用經(jīng)典邏輯刻畫(huà)， 比如使用 LTL或CTL刻畫(huà)系統(tǒng)的線性時(shí)間屬性。但存在一些現(xiàn)實(shí)世界用經(jīng) 典邏輯去刻畫(huà)是不完善的， 比如實(shí)時(shí)系統(tǒng)是一個(gè)非有窮狀態(tài)的計(jì) 算系統(tǒng)。為止，還有學(xué)者研究了非經(jīng)典模型檢測(cè)，例如概率系統(tǒng) 的模型檢測(cè) 1 、多值系統(tǒng)的模型檢測(cè) 2 、可能值系統(tǒng)的模型檢 測(cè)3 、量化系統(tǒng)的模型檢測(cè) 4-5 等。基于概率模型檢測(cè)主要應(yīng) 用于驗(yàn)證隨機(jī)系統(tǒng)中屬性可滿足概率， 它利用離散時(shí)間馬

4、爾可夫 鏈(Discrete Time Markov Cha in，DTMC 來(lái)刻畫(huà)模型，每一個(gè)狀態(tài)以一定的概率演化。概率計(jì)算樹(shù)邏輯( Probability Computational Tree Logic， PCTL)，則是對(duì) CTL進(jìn)行擴(kuò)展，用它來(lái)刻畫(huà)概率系統(tǒng)及其概率屬性 1，軟件PRISM就是解決這 類(lèi)問(wèn)題的概率模型檢測(cè)器。作為 CTL的另一種擴(kuò)展，加權(quán)的 CTL(Weighted Computational Tree Logic， WCTL 也備受關(guān)注，Brihaye 等6 、Bouyer7 重點(diǎn)研究了狀態(tài)和狀態(tài)轉(zhuǎn)移均賦以權(quán) 重的 CTL；Buchholz 等8 提出了基于半環(huán)的加權(quán)自動(dòng)機(jī)，將它 作為系統(tǒng)模型，以 WCTL作為刻畫(huà)系統(tǒng)屬性的邏輯，給出了系統(tǒng) 屬性檢測(cè)算法。關(guān)于加權(quán)遷移系統(tǒng)的線性時(shí)間屬性及其檢測(cè)算法， 目前還沒(méi) 有得到研究。 本文將在半環(huán)上提出加權(quán)遷移系統(tǒng)， 定義加權(quán)系統(tǒng) 的加權(quán)線性時(shí)間屬性，常見(jiàn)的有：加權(quán)安全性、加權(quán)HJ1.55mn 活性、 加權(quán)不變性等， 并且根據(jù)權(quán)重函數(shù)確定加權(quán)線性屬性的基 本性質(zhì)， 提出加權(quán)線性時(shí)間屬性的一般檢測(cè)方法。