确定的与非确定的公式时钟自动机的等价性

• 作者: 刘春霞
• 来源期刊: 科技信息
• 关键词: 公式记录时钟 公式预测时钟 时态算子 时间字
• 年，卷（期）: 2008,（17）
• 所属期刊栏目: 职校论坛2
• 页码范围: 596-597
• 页数: 2页
• 字数: 4302字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-9960.2008.17.457

摘要

本文分析了传统的时间自动机在实时系统进行形式化验证方面所存在的问题,提出了一种新的形式化验证工具--公式时钟自动机,给出了公式时钟自动机的形式化定义.在公式时钟自动机中,每一个事件对应一个命题、并且针对给定命题集上的每个时态公式,我们定义两个时钟:公式记录时钟与公式预测时钟.前者记录公式最近一次被满足时距目前的时间,后者预测下一次公式将被满足时距目前的时间.最后讨论了公式时钟自动机的确定性和非确定性,并证明了确定的公式时钟自动机和非确定的公式时钟自动机的等价性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘春霞		11	26	3.0	5.0