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

来源 :软件学报 | 被引量 : 0次 | 上传用户：xxx555xxx777

【摘要】

：

正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算,可以证明一个正则模型类在时态语言中可定义当且仅当它

【作者】

：

王善侠马明辉陈武邓辉文

【机构】

：

西南大学逻辑与智能研究中心,西南大学计算机与信息科学学院,河南师范大学计算机与信息工程学院

【出处】

：

软件学报

【发表日期】

：

2017年5期

【关键词】

：

正则模型时态语言 C2t-互模拟 C2t-超滤扩张时态可定义性 regular model temporal language C2t-bisimula

【基金项目】

：

国家社会科学基金重大项目（14ZDB016）

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

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

其他文献

计算机专业基础课程教学之我见

《计算机原理》、《计算机组装与维修》、《计算机网络技术》课程属于专业基础课程，在教学过程中必须从教学内容、教学过程、教学安排等方面进行全方位的优化，把握住教学内容的

期刊

计算机专业基础课程教学方法

基于运行特征监控的代码复用攻击防御

针对代码复用的攻击与防御已成为网络安全领域研究的热点,但当前的防御方法普遍存在防御类型单一、易被绕过等问题.为此,提出一种基于运行特征监控的代码复用攻击防御方法RCM

期刊

代码复用攻击运行特征系统调用插桩code reuse attack(CRA)running characteristicssystem calli

职业学校开展研究性学习的可行性探讨及设计

研究性学习是一种在教师指导下,学生以类似科学研究的方式,从自然、社会和自身生活中选择并确定主题,主动地获取知识、应用知识、解决问题的学习方式.研究性学习有五个特点:

期刊

研究性学习职业学校应用知识教师指导探究性学习方式学生社会综合性选择

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

其他学术论文