迁移系统关于一类时态逻辑公式的满足度  

Satisfaction degree for a class of temporal logic formulae based on transition systems

作　　者：王国俊[1] 王庆平[2] 时慧娴[1] 罗清君[1,3] 王伟[4] 

机构地区：[1]陕西师范大学数学与信息科学学院,陕西西安710062 [2]江西财经大学统计学院,江西南昌330013 [3]西安财经学院统计学院 [4]西安财经学院信息与教育技术中心,陕西西安710061

出　　处：《陕西师范大学学报（自然科学版）》2013年第4期1-10,共10页Journal of Shaanxi Normal University：Natural Science Edition

基　　金：国家自然科学基金资助项目(10771129;11171200)

摘　　要：从分析Words(φ)的结构入手,引入用线性时态逻辑(LTL)公式φ表示的规范的特征概念,证明了一类LTL公式特征的存在性定理以及特征的计算方法.引入了LTL公式的T-范式概念,证明了这类LTL公式均可等价地表示为T-范式的形式,从而为简化φ的特征计算奠定了基础.引入了迁移系统TS关于给定规范φ的满足度概念,证明了TS关于φ的满足度等于1当且仅当TS满足φ.对于给定的原子公式集AP,给出了满足度计算的复杂度估计.The concept of a character for lineal temporal logic （LTL, for short） formulae is introduced, and the existence of characters for a class of LTL formulae as well as the computation method are obtained. Based on this concept, two types of temporal normal form for LTL formulae are proposed, and it is proved that a class of LTL formulae can be equivalently expressed in temporal normal form, which greatly simplifies the complexity of computing of characters. Meanwhile, the satisfaction degree of LTL formulae with respect to transition systems are proposed, which can be seen as a quantitative extension of the notion ＂TS satisfies Ф＂. Finally, a computation method of the satisfaction degree for a LTL formula is provided, and the computation complexity is estimated.

关 键 词：规范 特征 最终自由 动态模型序列 T-范式 满足度 

分 类 号：O141.1[理学—数学]