基于自动机和可能性Kripke结构的模型检测理论应用研究

发布时间：2017-07-20 20:19

  本文关键词：基于自动机和可能性Kripke结构的模型检测理论应用研究

  更多相关文章： Buchi自动机 可能性测度 带有成本的可能性Kripke结构 多属性决策

【摘要】：在我们日常生活的各个方面,现代社会越来越依赖于专业的计算机和软件系统对于我们的协助。通常我们使用的手机,通信系统,医疗设备,音频和视频系统,以及家用电子产品一般都包含了大量的软件。一个常见的问题就是软硬件系统的复杂性不断增加,特别是有线和无线网络的使用更是加剧了这一趋势,所以计算机科学领域遇到的一个主要的挑战就是提供方法,技术和工具以确保正确且功能良好系统的有效设计。在过去的大约二十年里,针对基于计算机控制系统正确性验证的一个非常好的方法那就是模型检测。究竟什么是模型检测?我们从两个不同的角度给出定义：1.模型检测是一种主要的形式化验证技术用来评估信息和通信系统的功能性质；2.模型检测是在合适的系统模型上对系统期望的性质进行验证,验证过程就是对模型中所有的状态进行系统化的检查。 随着科技的进步,模型检测技术也在持续发展,从开始的经典模型检测到概率模型检测,再到今天的多值模型检测,量子模型检测和可能性模型检测,许多专家学者对这种形式化验证技术从理论到实践都做了大量的研究。如何把模型检测理论应用到实践以解决实际问题对于我们来说是至关重要的,本文将应用自动机模型对多处理器任务调度算法进行建模与验证。 成本(或者是收益)是人们在决策系统中关注的焦点。对于非可加性的决策问题,本文建立了带有成本(收益)的可能性测度概念,并研究了其期望测度和多属性决策。 本文主要工作如下： (1)提出了一个基于扩展Buchi自动机的形式化模型,并用该模型来描述多处理器任务调度算法TDS (Task Duplication based Scheduling);用线性时序逻辑描述出算法TDS期望的一些性质；最后在该模型上验证了这些性质。 (2)扩展了可能性Kripke结构——提出了带有成本的可能性Kripke结构,并且研究在此之上的期望测度和多属性决策问题。带有成本的可能性Kripke结构是在可能性Kripke结构的转移关系上(或者是状态上)给定了成本——这个自然数可以看成是成本,当然也可以看成是收益。本文中我们考虑转移关系上的成本。为了便于理解,我们会给出实例,将应用期望测度和最优化的理论来解决工程管理决策的相关问题。
【关键词】：Buchi自动机 可能性测度 带有成本的可能性Kripke结构 多属性决策
【学位授予单位】：陕西师范大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP332
【目录】：

• 摘要3-4
• Abstract4-6
• 目录6-7
• 第1章 前言7-11
• 第2章 预备知识11-19
• 2.1 Kripke结构11-12
• 2.2 Buchi自动机12-13
• 2.3 线性时序逻辑(LTL)的语法和语义13-14
• 2.4 计算树逻辑的语法与语义14-16
• 2.5 可能性Kripke结构16-17
• 2.6 基于可能性Kripke结构的计算树逻辑(PoCTL)17-18
• 2.7 本章小结18-19
• 第3章 多处理器任务调度算法TDS的建模与验证19-33
• 3.1 TDS算法介绍19-21
• 3.2 多处理器调度算法TDS的模型21-26
• 3.3 算法合理性描述26-27
• 3.4 扩展Buchi自动机对应的Kripke结构27
• 3.5 应用不动点算法进行模型检测27-31
• 3.6 本章小结31-33
• 第4章 基于可能性测度的工程管理决策的研究33-43
• 4.1 带有成本的可能性Kripke结构33-36
• 4.2 可达性质的期望成本(收益)36-37
• 4.3 多种属性的决策37-39
• 4.4 融合了成本的PoCTL—PoCCTL39-40
• 4.5 对于工程管理决策问题的验证40-41
• 4.6 本章小结41-43
• 总结43-45
• 参考文献45-49
• 致谢49-51
• 攻读硕士学位期间的研究成果51

【参考文献】

中国期刊全文数据库 前1条

1 徐泽水;基于期望值的模糊多属性决策法及其应用[J];系统工程理论与实践;2004年01期

，

本文编号：569833