一类时间自动机的时间约束可满足性判定方法

• 作者: 古天龙 廖伟志 董荣胜 蔡国永
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 时间自动机 时间约束 可满足性 实时系统
• 年，卷（期）: 2002,（13）
• 所属期刊栏目: 学术探讨
• 页码范围: 93-96
• 页数: 4页
• 分类号: TP31
• 字数: 4580字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2002.13.031

摘要

时间自动机是一种有效描述实时系统行为的计算模型.借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性.在此过程中对时间自动机的验证是非常关键的一步.验证的主要目的是为了保证时间自动机能够正确地描述实时系统.其中迁移的时间约束可满足性就是需要验证的性质之一.常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大.该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子工业学院计算机系	207	1546	18.0	30.0
2	蔡国永	桂林电子工业学院计算机系	98	400	12.0	15.0
3	董荣胜	桂林电子工业学院计算机系	115	1521	13.0	37.0
4	廖伟志	桂林电子工业学院计算机系	2	1	1.0	1.0