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

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