A Method for Linear Temporal Logic Programs Model Checking Based on Büchi Automaton

Formal verification of temporal logic programs plays an important role in improving program correctness.Corresponding Buchi Automaton is constructed based on automata theory,in which labeled transition system(S) indicating programs' acts,temporal logic formulas(F) indicating programs' property.Thus,it proves that whether formal formula SF is satisfiable or not.