摘要： 利用自动机理论模型检验算法，检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑，有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力，利用该方法对车站联锁逻辑的实际问题进行了性能验证。
关键词:
有色Petri网,
线性时态逻辑,
带标签的广义Büchi自动机,
联锁逻辑
Abstract: A method about automata-theoretic model checking is presented. This method is used to verify the property of color Petri nets(CPN) model of interlocking logic. State space exposition can be solved efficiently by constructing linear-time temporal logic(LTL) with labeled generalized Büchi automaton(LGBA) in model checking. This method improves the analysis and checking of CPN. A practical case of the railway interlocking logic is checked by this method.
Key words:
colored Petri nets,
linear-time temporal logic,
labeled generalized Büchi automaton,
interlocking logic
中图分类号:
杜军威;徐中伟;宋 波. 联锁逻辑形式化模型检验的研究[J]. 计算机工程, 2007, 33(15): 33-35.
DU Jun-wei; XU Zhong-wei; SONG Bo. Research on Formal Model Checking of Interlocking Logic[J]. Computer Engineering, 2007, 33(15): 33-35.