一种基于Büchi自动机的LTL程序模型检测方法  

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

作　　者：罗清胜[1] 

机构地区：[1]江西财经大学国际学院,江西南昌330013

出　　处：《计算机与现代化》2010年第8期58-61,共4页Computer and Modernization

摘　　要：时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论,用标签转移系统(S)表示程序的行为,用时序逻辑公式(F)描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足。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 SF is satisfiable or not.

关 键 词：线性时序逻辑 BÜCHI自动机 模型检测 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]