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

• 作者: 时慧娴 王伟 王国俊 王庆平 罗清君
• 来源期刊: 陕西师范大学学报（自然科学版）
• 学科: 数学
• 关键词: 规范 特征 最终自由 动态模型序列 T-范式 满足度
• 年，卷（期）: 2013,（4）
• 所属期刊栏目: 数学与计算机科学
• 页码范围: 1-10
• 页数: 10页
• 分类号: O141.1
• 字数: 13645字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王伟	西安财经学院信息与教育技术中心	52	125	7.0	8.0
2	王国俊	陕西师范大学数学与信息科学学院	176	2910	25.0	49.0
3	罗清君	陕西师范大学数学与信息科学学院	8	14	3.0	3.0
5	时慧娴	陕西师范大学数学与信息科学学院	7	21	3.0	4.0
8	王庆平	江西财经大学统计学院	5	10	2.0	3.0