关键词: 线性时序逻辑, Büchi自动机, 模型检测

Abstract: Formal verification of temporal logic programs plays an important role in improving program correctness. Corresponding Büchi 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 S |=F is satisfiable or not.

Key words: Linear time temporal logic, Büchi automaton, model checking