A Symbolic Optimization Method for Model Checking of LTL Based on Automaton Theory
Tianlong Gu · Jisuanji gongcheng · 2005
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 Buchi 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 Buchi 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.