正则模型类的时态可定义性

• 作者: 王善侠 邓辉文 陈武 马明辉
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 正则模型 时态语言 C2t-互模拟 C2t-超滤扩张 时态可定义性
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1070-1079
• 页数: 10页
• 分类号: TP301
• 字数: 9884字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005208

摘要

正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算,可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭,并且它的补类在C2t-超滤扩张下封闭,该刻画定理说明了时态语言在正则模型类上的表达力.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	邓辉文	西南大学逻辑与智能研究中心	34	339	12.0	17.0
5	马明辉	西南大学逻辑与智能研究中心	20	10	1.0	2.0
6	陈武	西南大学计算机与信息科学学院	9	24	4.0	4.0
7	王善侠	西南大学逻辑与智能研究中心	5	9	2.0	2.0