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.

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