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

摘要

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