基于CTL和Petri网的约束一致性验证方法研究

摘要：

通过分支时序逻辑(CTL)公式表示系统约束,利用Petri网的可达性分析技术来验证约束一致性是一种重要的、切实可行的约束一致性验证方法.文章描述了一种由CTL公式向Petri网映射的算法,将表示系统约束和组件约束的CTL公式分别映射为Petri网,然后利用Petri网的组合、可达性分析等技术从语义上来验证系统约束与组件约束的一致性.最后,通过对算法的实现开发了一个工具包,并通过一个实例验证了算法正确性和约束一致性验证方法的可行性.

关键词：CTL、Petri Net、约束、一致性

所属期刊栏目：42

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金NSFC:60474026;清华大学校科研和教改项目

在线出版日期：2006-09-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：52-57