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

摘要：

从分析Words(ρ)的结构入手,引入用线性时态逻辑(LTL)公式ρ表示的规范的特征概念,证明了一类LTL公式特征的存在性定理以及特征的计算方法.引入了LTL公式的T-范式概念,证明了这类LTL公式均可等价地表示为T-范式的形式,从而为简化ρ的特征计算奠定了基础.引入了迁移系统TS关于给定规范ρ的满足度概念,证明了TS关于ρ的满足度等于1当且仅当TS满足ρ.对于给定的原子公式集AP,给出了满足度计算的复杂度估计.

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

所属期刊栏目：41

分类号：O141.1(数理逻辑、数学基础)

资助基金：国家自然科学基金资助项目10771129,11171200

在线出版日期：2013-10-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1-10