On the specification of modal systems: A comparison of three frameworks
Luca Aceto, Ignacio Fábregas, David de Frutos Escrig, Anna Ingólfsdóttir, Miguel Palomino
TL;DR
This work analyzes three behavioural preorders—modal refinement on modal transition systems (MTS), covariant-contravariant simulation (cc) on labelled transition systems (LTS), and partial bisimulation (PB)—and develops mutual translations between MTS and LTS that preserve and reflect these preorders and their associated modal logics. It introduces a translation M from LTS to MTS and a translation C from MTS to LTS, proving that cc corresponds to refinement under M and that refinement corresponds to cc under C, while also extending these translations to preserve formula satisfaction. The paper further shows how characteristic formulae can be transferred across the translations, providing logical characterizations that underpin model-checking approaches, and situates the whole framework within an institutional ( Burstall-Goguen) perspective by defining two related institutions and an institution morphism. It also analyzes PB in relation to cc and MTS, revealing expressiveness gaps and the limits of embeddings between the formalisms. Overall, the results establish MTS as a unifying framework that embeds LTS under cc and PB, enabling cross-pollination of expressive power, verification techniques, and supervisory-control insights across the three formalisms.
Abstract
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.