有限精度时间自动机的时钟表示

• 作者: 刘春明 徐雨波 晏荣杰
• 来源期刊: 计算机应用研究
• 关键词: 有限精度时间自动机 模型检验 符号化方法
• 年，卷（期）: 2006,（7）
• 所属期刊栏目: 研究探讨
• 页码范围: 23-25,31
• 页数: 4页
• 分类号: TP301.1
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2006.07.006

摘要

简要介绍了有限精度时间自动机(FPTA)的基本概念,重点讨论FPTA状态中时钟的表示.FPTA只记录时钟值的整数部分,而用时钟序的概念来模拟表示时钟值小数部分的大小关系,从而减少生成的状态空间.在FPTA模型中,时钟操作的时空性能主要依赖于时钟序的数据结构和算法.提出了用位矩阵来表示时钟序的数据结构POM(Partial-Order Matrix).采用该结构的操作算法具有O(n)复杂度,且无需标准化操作;同时,一切操作均可以通过位运算实现,从而大幅度提高时钟操作的时间效率.