%0 Journal Article
%T Property patterns of linear temporal logics<br>线性时态逻辑中的特性模式
%A LI Sheng-hong
%A MIAO Huai-kou
%A ZHANG Xin-lin
%A <br>黎升洪
%A 缪淮扣
%A 张新林
%J 计算机应用
%D 2006
%I 
%X 在模型检查应用中，需要使用线性时态逻辑对软件具备的特性进行描述。虽然，不同应用背景涉及不同方面的特性描述，但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性，首先，按照线性时态逻辑所描述性质划分，常见性质包括活性、安全性等；其次，按照线性时态逻辑公式的作用范围划分。通过对共同问题，找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。
%K SPIN<br>线性时态逻辑
%K 特性模式
%K 模型检查
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=831E194C147C78FAAFCC50BC7ADD1732&aid=86E270690350FDDD&yid=37904DC365DD7266&vid=96C778EE049EE47D&iid=5D311CA918CA9A03&sid=E1E3BF53C3583450&eid=E1BA6CA93A8F9A6A&journal_id=1001-9081&journal_name=计算机应用&referenced_num=0&reference_num=9