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

基于时间自动机若干新模型的研究

作　者: 朱维军
导　师: 周清雷
学　校: 郑州大学
专　业: 计算机应用技术
关键词: 时间自动机时间树自动机信号自动机基因网络离散步长双向模拟识别语言
分类号: TP301.1
类　型: 硕士论文
年　份: 2005年
下　载: 199次
引　用: 5次
阅　读: 论文下载

内容摘要

时间自动机被广泛用于实时系统验证和模型检测。一方面出现了很多算法和工具;另一方面有不少基于时间自动机的不同模型被提出,以适应不同类型的系统验证。信号自动机与时间树自动机是两个新提出的模型。时间树自动机理论还很不完善,目前主要是基于时间树自动机识别的语言类及相关性质的研究。本文提出了一个时间树自动机识别语言的一个条件,并证明了结论的正确性。如果一个语言不能满足该条件,它一定不能被时间树自动机识别。这为证明一个具体语言不能被时间树自动机识别提供了思路。信号自动机为一类实时系统建立了比普通时间自动机更适合的模型。本文通过对信号自动机与时间自动机的模型对比与深入分析,证明了两种模型的行为等价关系,并提出了互模拟算法,这样信号自动机验证问题被归约为时间自动机验证问题。如果把这样的互模拟算法与时间自动机验证算法组合在一起,就可以得到信号自动机验证算法,以便在此基础上开发出信号自动机验证工具。在基因工程中,形式化方法被用于预测人工基因网络控制生物基因网络的行为结果,这种预测已经在生物医药研制与开发领域发挥了很大作用。目前已有的基于有限状态自动机的方法的局限是不能描述系统时间约束。本文提出了基于时间自动机的基因网络逻辑模型,以计算时间约束下控制基因网络的行为。

全文目录

摘要  3-4
ABSTRACT  4-7
引言  7-11
  1、研究背景与研究现状  7-9
  2、研究内容和研究意义  9
  3、本文结构  9-11
第一章时间自动机  11-24
  1．1 时间语言  11-12
  1．2 时间约束和时钟解释  12
  1．3 时间自动机的语法和语义  12-14
  1．4 时间正则语言  14-15
  1．5 确定型时间自动机  15-16
  1．6 区域自动机  16-19
    1．6．1 时钟区域  16-17
    1．6．2 区域自动机  17-19
  1．7 带自动机  19-21
  1．8 时间正则表达式  21-22
    1．8．1 语法  21
    1．8．2 语义  21-22
    1．8．3 时间自动机的Kleene定理  22
  1．9 时间自动机识别语言的一个条件定理  22-24
第二章时间树自动机  24-38
  2．1 运行在无穷树上的自动机  24-26
  2．2 时间树自动机  26-28
  2．3 时间树自动机的区域构造  28-29
  2．4 时间树语言类的关系  29-30
  2．5 封闭性和判定问题  30-31
  2．6 应用  31-35
  2．7 时间树自动机识别语言的一个条件定理  35-38
第三章信号自动机  38-46
  3．1 信号  38-40
  3．2 信号自动机与信号正则表达式  40-41
  3．3 时间自动机与信号自动机行为的等价性  41-43
  3．4 离散步长双向模拟算法  43-46
    3．4．1 从SA到TA  43-44
    3．4．2 从TA到SA  44
    3．4．3 对算法的说明  44-46
第四章基于时间自动机的实时系统验证  46-54
  4．1 使用时间自动机验证  46-47
  4．2 一个实例:使用验证工具KRONOS验证CSMA/CD协议  47-54
    4．2．1 KRONOS工具介绍  47-48
    4．2．2 为CSMA/CD协议建模  48-50
    4．2．3 使用TCTL逻辑验证  50-51
    4．2．4 基于KRONOS的验证  51-52
    4．2．5 验证CSMA/CD协议  52-54
第五章应用研究:基于时间自动机的基因网络逻辑模型  54-58
  5．1 基于有限状态自动机的基因网络模型  54-55
  5．2 基于时间自动机的基因网络模型  55-58
第六章结束语  58-59
致谢  59-60
参考文献  60-67
附录1 攻读硕士学位期间发表的论文  67

基于时间自动机若干新模型的研究

内容摘要

全文目录

相似论文