| 王善侠,马明辉,陈武,邓辉文.正则模型类的时态可定义性.软件学报,2017,28(5):1070-1079 |
| 正则模型类的时态可定义性 |
| Temporal Definability of Regular Model Classes |
| 投稿时间：2016-06-30 修订日期：2016-09-25 |
| DOI：10.13328/j.cnki.jos.005208 |
| 中文关键词: 正则模型 时态语言 C2t-互模拟 C2t-超滤扩张 时态可定义性 |
| 英文关键词:regular model temporal language C2t- bisimulation C2t- ultrafilter extension temporal definability |
| 基金项目:国家社会科学基金重大项目（14ZDB016） |
|
| 摘要点击次数: 1844 |
| 全文下载次数: 1247 |
| 中文摘要: |
| 正则模型是非正规模态逻辑的模型，通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算，可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭，并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力. |
| 英文摘要: |
| 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. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
