【摘要】：隨機(jī)切換系統(tǒng)是離散狀態(tài)、連續(xù)狀態(tài)和隨機(jī)因素相互交織的一類系統(tǒng),這類系統(tǒng)被廣泛應(yīng)用于工業(yè)控制、導(dǎo)航系統(tǒng)、飛行器控制系統(tǒng)、空中交通系統(tǒng)、股票市場模型中。由于描述離散切換邏輯和隨機(jī)連續(xù)動態(tài)的語言是不同的,這使得建立一個統(tǒng)一的模型進(jìn)行設(shè)計和分析變得更加困難。 本文研究了這樣一類隨機(jī)切換系統(tǒng),它的連續(xù)動態(tài)用Ito隨機(jī)微分方程描述,而控制邏輯是基于Markov跳躍的。文章實現(xiàn)了對這類系統(tǒng)的形式化建模與分析。本文首先定義了一種新的Petri網(wǎng)模型——隨機(jī)可微Petri網(wǎng),這種新Petri網(wǎng)可以實現(xiàn)離散邏輯與連續(xù)動態(tài)的統(tǒng)一建模；本文采用這種Petri網(wǎng),基于E-M離散格式,實現(xiàn)了對基于Markov控制的隨機(jī)切換系統(tǒng)的形式化建模。在此基礎(chǔ)上,本文采用模型檢查工具PRISM對所建立的模型進(jìn)行檢查。為了實現(xiàn)對模型的檢查,本文構(gòu)造了Petri網(wǎng)可達(dá)圖對應(yīng)的Markov鏈,并且證明了這個Markov鏈與系統(tǒng)狀態(tài)空間對應(yīng)的Markov鏈?zhǔn)堑葍r的,在此基礎(chǔ)上采用模型檢查工具PRISM對其進(jìn)行模型檢查。為了說明文章所介紹的方法的正確性和有效性,本文給出了具有恒溫器的房間溫度變化的例子的建模與分析。 本文的貢獻(xiàn)如下： (1)實現(xiàn)了對隨機(jī)因素的建模；本文建立的隨機(jī)可微Petri網(wǎng)模型可以同時描述離散切換邏輯和具有隨機(jī)因素的連續(xù)動態(tài)； (2)實現(xiàn)了對具有無限狀態(tài)的系統(tǒng)的模型檢查,將無限的狀態(tài)映射成有限狀態(tài),使其可以用于模型檢查工具；
【學(xué)位授予單位】：浙江理工大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2013
【分類號】：N945.12;TP301.1

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 劉路路;陶玲;;數(shù)字系統(tǒng)的形式化驗證方法[J];合肥師范學(xué)院學(xué)報;2008年03期

2 戴毅茹;王堅;;Towards Production and Energy Coupling System Modeling and Simulation for Energy Optimization in the Process Industry[J];Journal of Donghua University(English Edition);2011年02期

3 戴志輝;王增平;;微機(jī)保護(hù)動作邏輯建模與動態(tài)分析[J];電力系統(tǒng)自動化;2009年11期

4 譚娟;李陽;劉鳳麗;;基于模糊微分Petri網(wǎng)的混合系統(tǒng)表示[J];工業(yè)控制計算機(jī);2011年12期

5 范德會;馬光勝;;林業(yè)機(jī)械設(shè)備控制芯片設(shè)計的模型檢驗方法[J];東北林業(yè)大學(xué)學(xué)報;2013年02期

6 耿曉晶;;多維馬爾科夫轉(zhuǎn)制隨機(jī)微分方程的數(shù)值解[J];純粹數(shù)學(xué)與應(yīng)用數(shù)學(xué);2013年06期

7 楊東;趙軍;;一類帶有執(zhí)行器故障的隨機(jī)跳躍系統(tǒng)的可靠控制[J];東北大學(xué)學(xué)報(自然科學(xué)版);2015年02期

8 魚先鋒;雷麗暉;李永明;;單道批處理系統(tǒng)的建模與驗證[J];計算機(jī)科學(xué);2011年04期

9 戴毅茹;王堅;;多耦合混雜流程工業(yè)過程可重構(gòu)建模方法[J];計算機(jī)集成制造系統(tǒng);2011年11期

10 翟長連,吳智銘;基于不變集的一類混合系統(tǒng)的穩(wěn)定性[J];控制與決策;2000年06期

相關(guān)會議論文 前2條

1 Suxia Ding;Dianfeng Zhang;Zhaojing Wu;;Stability of a class of stochastic switched systems with time delays[A];第25屆中國控制與決策會議論文集[C];2013年

2 Wu-Hua Chen;Chenghai Wei;Xiaomei Lu;;Mean Square Exponential Stability of Uncertain Linear Impulsive Stochastic Systems with Markovian Switching[A];第25屆中國控制與決策會議論文集[C];2013年

相關(guān)博士學(xué)位論文 前10條

1 翟海峰;混雜系統(tǒng)分析與控制設(shè)計研究[D];浙江大學(xué);2001年

2 尹增山;混雜系統(tǒng)優(yōu)化控制理論研究[D];浙江大學(xué);2001年

3 葉陽東;智能混雜系統(tǒng)建模、分析理論及應(yīng)用的研究[D];鐵道部科學(xué)研究院;2002年

4 李衛(wèi)東;混雜動態(tài)系統(tǒng)的分析與控制[D];浙江大學(xué);2003年

5 郅躍茹;混合動態(tài)系統(tǒng)中幾個關(guān)鍵技術(shù)的研究[D];浙江大學(xué);2005年

6 魯巍;模擬驗證中的激勵產(chǎn)生與覆蓋評估[D];中國科學(xué)院研究生院（計算技術(shù)研究所）;2006年

7 楊軍;集成電路的邏輯等價性驗證研究[D];浙江大學(xué);2007年

8 趙景波;汽車EPS混雜控制系統(tǒng)理論、設(shè)計及實現(xiàn)研究[D];江蘇大學(xué);2009年

9 張博;可外接充電混合動力汽車能量管理策略研究[D];吉林大學(xué);2009年

10 王鮮芳;生化過程動態(tài)建模及優(yōu)化控制研究[D];江南大學(xué);2009年

相關(guān)碩士學(xué)位論文 前10條

1 周清;基于混合Petri網(wǎng)的列車運(yùn)行系統(tǒng)中時間推理問題的研究[D];鄭州大學(xué);2010年

2 魚先鋒;單道批處理系統(tǒng)建模與驗證[D];陜西師范大學(xué);2011年

3 萬上宏;基于重用驗證方法學(xué)的信道重編碼系統(tǒng)功能驗證研究[D];華南理工大學(xué);2011年

4 田釗;基于一類混合Petri網(wǎng)的列車運(yùn)行系統(tǒng)中沖突因素的分析[D];鄭州大學(xué);2011年

5 邱曉光;AVS視頻解碼芯片功能驗證平臺的研究與實現(xiàn)[D];山東大學(xué);2011年

6 李婧;SMT求解器技術(shù)對比分析及其能力擴(kuò)展研究[D];國防科學(xué)技術(shù)大學(xué);2010年

7 陳哲;基于OVM的集成電路驗證技術(shù)研究與應(yīng)用[D];北京郵電大學(xué);2012年

8 陳江紅;基于混合Petri網(wǎng)的混雜系統(tǒng)建模及工業(yè)應(yīng)用研究[D];北京化工大學(xué);2004年

9 彭昭;混雜系統(tǒng)的半定性故障診斷方法研究[D];清華大學(xué);2004年

10 夏曉菲;超大規(guī)模專用集成電路的功能仿真和驗證[D];華中科技大學(xué);2004年

，

本文編號：2623565