陕西师范大学学报（自然科学版）2013，Vol.41Issue(4)：1-10,10.
迁移系统关于一类时态逻辑公式的满足度
Satisfaction degree for a class of temporal logic formulae based on transition systems
摘要
Abstract
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-范式/满足度Key words
specification/ character/ eventually free/ dynamic model sequence/ temporal normal form/ satisfaction degree分类
数理科学引用本文复制引用
王国俊,王庆平,时慧娴,罗清君,王伟..迁移系统关于一类时态逻辑公式的满足度[J].陕西师范大学学报（自然科学版）,2013,41(4):1-10,10.基金项目
国家自然科学基金资助项目(10771129,11171200). （10771129,11171200）
