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

发布时间：2018-06-13 20:30

本文选题：正则模型 + 时态语言　；参考：《软件学报》2017年05期

【摘要】：正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算,可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭,并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力.
[Abstract]:A regular model is a model of irregular modal logic. By defining the disjoint of regular models, C2t- intersimulation, generating submodels, and C2t- ultrafiltration expansion and other models, it can be proved that a regular model class can be defined in the temporal language if and only if it is not intersected and is full of C2t- interanalog images and C2t- ultrafiltration expansion is closed, and Its complement classes are closed under C2t- ultrafiltration expansion. The characterization theorem illustrates the expressive power of temporal languages on regular model classes.
【作者单位】：西南大学逻辑与智能研究中心;河南师范大学计算机与信息工程学院;西南大学计算机与信息科学学院;
【基金】：国家社会科学基金重大项目(14ZDB016)~~
【分类号】：O141

【相似文献】