This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant-contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that preserve, and reflect, refinement and the covariant-contravariant simulation preorder. The translations are also shown to preserve the modal properties that can be expressed in the logics that characterize those preorders. A translation from labelled transition systems modulo the partial bisimulation preorder into the same model modulo the covariant-contravariant simulation preorder is also offered, together with some evidence that the former model is less expressive than the latter. In order to gain more insight into the relationships between modal transition systems modulo refinement and labelled transition systems modulo the covariant-contravariant simulation preorder, their connections are also phrased and studied in the context of institutions.

翻译：本文研究文献中提出的三种行为预序关系：模态迁移系统上的精化关系、标注迁移系统上的协变-逆变模拟预序与部分互模拟预序。研究表明，模态迁移系统与标注迁移系统之间存在可保持并反映精化关系与协变-逆变模拟预序的互译转换。这些转换同时保持了刻画这些预序的逻辑中可表达的模态性质。本文还给出了从部分互模拟预序下标注迁移系统到协变-逆变模拟预序下同一模型的转换，并提供证据表明前者的表达能力弱于后者。为深入理解模态迁移系统（模精化）与标注迁移系统（模协变-逆变模拟预序）之间的关系，本文还在制度框架下对其关联性进行了形式化表述与研究。