学位论文 > 优秀研究生学位论文题录展示

时间自动机新的识别模型及对长跨度区域自动机的研究

作　者: 郑丽萍
导　师: 周清雷
学　校: 郑州大学
专　业: 计算机软件与理论
关键词: 时间字 时间自动机 时间语言 长跨度区域自动机 时间后继
分类号: TP23
类　型: 硕士论文
年　份: 2001年
下　载: 66次
引　用: 1次
阅　读: 论文下载
 

内容摘要


经典的ω-有穷自动机用于系统验证时抽离了时间特性，不适用于研究与物理过程发生交互的系统。时间自动机扩充时间因素于经典ω-有穷自动机，从而把握实时系统的行为，提供有穷控制实时系统的验证和特定时间延迟问题的解决方案。目前已成为对实时并发系统进行模拟和验证的有效工具，广泛应用于时态逻辑、Petri网、协议验证和回路验证等。 时间自动机理论的一个重要方面是时间自动机在不同识别条件下识别时间语言的能力及时间语言在布尔运算下的封闭性。不同识别条件决定不同的时间自动机识别模型。目前对时间自动机仅讨论了C1，C5，C3，E，I，L条件下的识别模型。本文提出并深入讨论提出另四种经典识别条件C2，C3，C4，C6和对Ci（i=1…6）取反所得新条件下的时间自动机识别模型。 时间自动机用于实时验证的关键步骤是区域自动机的构造。经典区域自动机模型存在如下缺陷：时钟常量取值限制在有理数范围不合理；时钟区域划分过于细小，与时间自动机对应关系不直接。本文提出一种新的区域自动机模型；长跨度区域自动机。该模型允许时钟常量取实数值，并增大时钟区域的时间跨度，从而简化构造步骤，取得较优的时间和空间复杂度。这将极大提高实时验证的效率。

全文目录


中文摘要  3-4
英文摘要  4-5
第一章 问题描述  5-19
  1．1 ω-有穷自动机理论综述  5-11
  1．2 时间自动机理论综述  11-18
  1．3 问题描述  18-19
第二章 时间自动机新的识别模型  19-30
  2．1 时间语言和时间转换表  19-22
  2．2 时间自动机及其识别条件  22-24
  2．3 时间自动机在CI，┓CI（I=1，…6）下的识别模型  24-30
第三章 长跨度区域自动机  30-44
  3．1 经典区域自动机的定义及构造  30-38
  3．2 长跨度区域自动机  38-44
第四章 总结与展望  44-45
致谢  45-46
参考文献  46-47

相似论文

  1. 基于时间自动机模型的CBTC系统安全计算机平台的形式化验证,U284.48
  2. 基于时间自动机的模型验证技术,TP301.1
  3. 基于MDE的UML模型到形式化模型的转换方法研究,TP311.52
  4. IF对实时软件设计图形模型的验证,TP311.52
  5. 分布式实时系统调度分析工具的改进研究,TP311.52
  6. 基于时间自动机的CTCS-3级列控车载设备建模与验证,U284.48
  7. 基于XYZ/ADL的Web服务组合验证研究,TP393.09
  8. 场独立与场依赖型风格学习者的口语产出研究,H319
  9. 基于Petri网的嵌入式系统建模与验证研究,TP368.1
  10. FLASH存储器字线电压发生器优化设计,TN86
  11. 基于时间自动机的可生存性评估方法研究,TP393.08
  12. 基于UPPAAL的联锁进路控制流程建模与验证,U284.37
  13. 基于时间自动机的RBC控车流程研究,U284.48
  14. 一种针对基于构件的嵌入式实时软件的测试方法,TP311.52
  15. 基于公钥加密体制的SIP协议安全模型研究与实现,TP311.52
  16. 任务前准备时间对中国中级和高级英语学习者自我纠正的影响,H319
  17. 实时系统模型检测工具FPTAT的算法与实现,TP311.5
  18. 基于时间自动机若干新模型的研究,TP301.1
  19. 公式时钟自动机,TP311.52
  20. 基于SIP的视频会议服务器的设计、实现与分析,TP368.5

中图分类: > 工业技术 > 自动化技术、计算机技术 > 自动化技术及设备 > 自动化装置与设备
© 2012 www.xueweilunwen.com