發(fā)布時(shí)間：2017-07-20 20:19

  本文關(guān)鍵詞：基于自動(dòng)機(jī)和可能性Kripke結(jié)構(gòu)的模型檢測理論應(yīng)用研究

  更多相關(guān)文章： Buchi自動(dòng)機(jī) 可能性測度 帶有成本的可能性Kripke結(jié)構(gòu) 多屬性決策

【摘要】：在我們?nèi)粘Ｉ畹母鱾�(gè)方面,現(xiàn)代社會越來越依賴于專業(yè)的計(jì)算機(jī)和軟件系統(tǒng)對于我們的協(xié)助。通常我們使用的手機(jī),通信系統(tǒng),醫(yī)療設(shè)備,音頻和視頻系統(tǒng),以及家用電子產(chǎn)品一般都包含了大量的軟件。一個(gè)常見的問題就是軟硬件系統(tǒng)的復(fù)雜性不斷增加,特別是有線和無線網(wǎng)絡(luò)的使用更是加劇了這一趨勢,所以計(jì)算機(jī)科學(xué)領(lǐng)域遇到的一個(gè)主要的挑戰(zhàn)就是提供方法,技術(shù)和工具以確保正確且功能良好系統(tǒng)的有效設(shè)計(jì)。在過去的大約二十年里,針對基于計(jì)算機(jī)控制系統(tǒng)正確性驗(yàn)證的一個(gè)非常好的方法那就是模型檢測。究竟什么是模型檢測?我們從兩個(gè)不同的角度給出定義：1.模型檢測是一種主要的形式化驗(yàn)證技術(shù)用來評估信息和通信系統(tǒng)的功能性質(zhì)；2.模型檢測是在合適的系統(tǒng)模型上對系統(tǒng)期望的性質(zhì)進(jìn)行驗(yàn)證,驗(yàn)證過程就是對模型中所有的狀態(tài)進(jìn)行系統(tǒng)化的檢查。 隨著科技的進(jìn)步,模型檢測技術(shù)也在持續(xù)發(fā)展,從開始的經(jīng)典模型檢測到概率模型檢測,再到今天的多值模型檢測,量子模型檢測和可能性模型檢測,許多專家學(xué)者對這種形式化驗(yàn)證技術(shù)從理論到實(shí)踐都做了大量的研究。如何把模型檢測理論應(yīng)用到實(shí)踐以解決實(shí)際問題對于我們來說是至關(guān)重要的,本文將應(yīng)用自動(dòng)機(jī)模型對多處理器任務(wù)調(diào)度算法進(jìn)行建模與驗(yàn)證。 成本(或者是收益)是人們在決策系統(tǒng)中關(guān)注的焦點(diǎn)。對于非可加性的決策問題,本文建立了帶有成本(收益)的可能性測度概念,并研究了其期望測度和多屬性決策。 本文主要工作如下： (1)提出了一個(gè)基于擴(kuò)展Buchi自動(dòng)機(jī)的形式化模型,并用該模型來描述多處理器任務(wù)調(diào)度算法TDS (Task Duplication based Scheduling);用線性時(shí)序邏輯描述出算法TDS期望的一些性質(zhì)；最后在該模型上驗(yàn)證了這些性質(zhì)。 (2)擴(kuò)展了可能性Kripke結(jié)構(gòu)——提出了帶有成本的可能性Kripke結(jié)構(gòu),并且研究在此之上的期望測度和多屬性決策問題。帶有成本的可能性Kripke結(jié)構(gòu)是在可能性Kripke結(jié)構(gòu)的轉(zhuǎn)移關(guān)系上(或者是狀態(tài)上)給定了成本——這個(gè)自然數(shù)可以看成是成本,當(dāng)然也可以看成是收益。本文中我們考慮轉(zhuǎn)移關(guān)系上的成本。為了便于理解,我們會給出實(shí)例,將應(yīng)用期望測度和最優(yōu)化的理論來解決工程管理決策的相關(guān)問題。
【關(guān)鍵詞】：Buchi自動(dòng)機(jī) 可能性測度 帶有成本的可能性Kripke結(jié)構(gòu) 多屬性決策
【學(xué)位授予單位】：陜西師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP332
【目錄】：

• 摘要3-4
• Abstract4-6
• 目錄6-7
• 第1章 前言7-11
• 第2章 預(yù)備知識11-19
• 2.1 Kripke結(jié)構(gòu)11-12
• 2.2 Buchi自動(dòng)機(jī)12-13
• 2.3 線性時(shí)序邏輯(LTL)的語法和語義13-14
• 2.4 計(jì)算樹邏輯的語法與語義14-16
• 2.5 可能性Kripke結(jié)構(gòu)16-17
• 2.6 基于可能性Kripke結(jié)構(gòu)的計(jì)算樹邏輯(PoCTL)17-18
• 2.7 本章小結(jié)18-19
• 第3章 多處理器任務(wù)調(diào)度算法TDS的建模與驗(yàn)證19-33
• 3.1 TDS算法介紹19-21
• 3.2 多處理器調(diào)度算法TDS的模型21-26
• 3.3 算法合理性描述26-27
• 3.4 擴(kuò)展Buchi自動(dòng)機(jī)對應(yīng)的Kripke結(jié)構(gòu)27
• 3.5 應(yīng)用不動(dòng)點(diǎn)算法進(jìn)行模型檢測27-31
• 3.6 本章小結(jié)31-33
• 第4章 基于可能性測度的工程管理決策的研究33-43
• 4.1 帶有成本的可能性Kripke結(jié)構(gòu)33-36
• 4.2 可達(dá)性質(zhì)的期望成本(收益)36-37
• 4.3 多種屬性的決策37-39
• 4.4 融合了成本的PoCTL—PoCCTL39-40
• 4.5 對于工程管理決策問題的驗(yàn)證40-41
• 4.6 本章小結(jié)41-43
• 總結(jié)43-45
• 參考文獻(xiàn)45-49
• 致謝49-51
• 攻讀碩士學(xué)位期間的研究成果51

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

1 徐澤水;基于期望值的模糊多屬性決策法及其應(yīng)用[J];系統(tǒng)工程理論與實(shí)踐;2004年01期

，

本文編號：569833