%0 Journal Article
%T Model Checking for Temporal Logic Programs<br>时序逻辑程序的模型检测
%A WANG Xiao-bing
%A DUAN Zhen-hua
%A <br>王小兵
%A 段振华
%J 计算机科学
%D 2009
%I 
%X 时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序p和性质Ф统一表示在投影时序逻辑中,模型检测需要判定p→Ф是否有效,可转化为判定p∧Ф是否不可满足,这可以通过构造p∧Ф的正则图加以解决。最后,给出了Framed Tempura程序的模型检测实例。
%K Temporal logic programs
%K Formal verification
%K Normal form graphs
%K Model checking<br>时序逻辑程序
%K 形式化验证
%K 正则图
%K 模型检测
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=FABDAA6CAA3DA05995A7C59A6ACFF0C7&yid=DE12191FBD62783C&vid=933658645952ED9F&iid=F3090AE9B60B7ED1&sid=F260CE035846B3B8&eid=ED01F5AE50BE09C0&journal_id=1002-137X&journal_name=计算机科学&referenced_num=2&reference_num=9