文摘
英文文摘
郑重声明
第一章引言
1.1有穷状态自动机的提出
1.2时间自动机
1.3模型验证
1.4论文内容及结构
第二章公式时钟自动机
2.1线性命题时态逻辑公式的语法
2.2线性命题时态逻辑公式的语义
2.3公式记录时钟与公式预测时钟
2.4公式时钟自动机的语法和语义
第三章确定性与非确定性公式时钟自动机的等价性
3.1确定的公式时钟自动机
3.2确定性与非确定性公式时钟自动机的等价性
第四章公式时钟自动机的性质
4.1用标记变换系统描述公式时钟自动机的语义
4.2公式时钟自动机的域构造
4.3公式时钟自动机在布尔运算下的封闭性
4.4公式时钟Büchi自动机与公式时钟Muller自动机
4.5公式时钟自动机与事件时钟自动机之间的关系
第五章用公式时钟自动机进行验证
5.1轨迹语义
5.2给轨迹加上时间
5.3 ω自动机与验证
5.4用公式时钟自动机进行验证
5.5验证举例
第六章总结与展望
6.1总结
6.2展望
致谢
参考文献
发表论文
