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

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

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

【參考文獻】

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

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

，

本文編號：569833