正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、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.