摘要： 模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。

关键词: 线性时态逻辑, ω自动机, Büchi自动机, ROBDD

Abstract: Model checking is one of the most practical techniques of automatic formal verification to ensure the correctness of design specifications.To check whether a model satisfies a linear time temporal logic(LTL) formula,this proposes a method to translate a Büchi automata from LTL.The problem of formal verification of systems can be converted into a problem of checking containment of language received by implementation automaton and specification automata.However,it is very important for model checking to reduce the size of the automata.For optimization the Büchi automata derived from LTL properties,it gives an improved method that applies rewriting the formula before translation,and then reduces the number of states generated by the translation via Boolean optimization based on ROBDD.The results suggest that reduction of the state space is efficient.

中图分类号: 

• TP301