Property patterns of linear temporal logics
线性时态逻辑中的特性模式

在模型检查应用中，需要使用线性时态逻辑对软件具备的特性进行描述。虽然，不同应用背景涉及不同方面的特性描述，但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性，首先，按照线性时态逻辑所描述性质划分，常见性质包括活性、安全性等；其次，按照线性时态逻辑公式的作用范围划分。通过对共同问题，找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。