首页> 中文期刊> 《软件学报》 >正则模型类的时态可定义性

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

         

摘要

Regular models are models for non-normal modal logics.By defining some model operations,including disjoint union,C2t-bisimulation,generated submodel,and C2t-ultrafilter extension,this study proves that a class of regular models can be defined in the temporal language if and only if it is closed under disjoint unions,surjective C2t-bisimulations and C2t-ultrafilter extensions,while its complement is closed under ultrafilter extensions.This characterization theorem explains the expressive power of temporal language over regular models.%正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算,可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭,并且它的补类在C2t-超滤扩张下封闭,该刻画定理说明了时态语言在正则模型类上的表达力.

著录项

相似文献

  • 中文文献
  • 外文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号