摘要： 首先基于模型上的模拟概念定义了模型上的双模拟概念，并给出双模拟模态不变性和模态等价性的定义。在此基础上，讨论了模态逻辑与双模拟之间的关系；进一步分别在语言ＭＬ（τ，Φ）和ＭＬ∞（τ，Φ）中分析了模态等价性与双模拟不变性之间的关系；最后证明了正存在模态公式与双模拟之间的关系，并把正存在模态公式刻画为一阶公式双模拟不变部分。