摘要
利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证。
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 Btichi 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.
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第15期33-35,共3页
Computer Engineering
基金
国家自然科学基金资助项目(60674004)
