联锁逻辑形式化模型检验的研究

摘要：

利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能.通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题.该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证.

关键词：有色Petri网、线性时态逻辑、带标签的广义Büchi自动机、联锁逻辑

所属期刊栏目：33

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

资助基金：国家自然科学基金60674004

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

页数：共3页

页码：33-35