In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed in 1992 that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones.

This talk present the extension of that classical result from a purely logical point of view, but with an eye over the behavioural preorders in van Glabbeek’s linear-time branching-time spectrum. It will be shown general and sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones will be shown. As a first step towards the general result, the property is translated to the scenario of covariant-contravariant simulations over label transition systems. Finally, there will be a look into a promising direction that the speaker is exploring based in one recent paper of Legay and Fahrenberg also inspired by the foundational paper of Boudol and Larsen.