In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed 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 paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek's branching-time spectrum.

翻译：在刻画模态转移系统上模态精化的模态逻辑背景下，Boudol和Larsen证明：可将模型检测归约为预序检测的公式（即特征公式）恰好是那些一致且素公式。本文给出了保证特征公式恰好为一致且素公式的通用充分条件，并证明所给条件适用于刻画van Glabbeek分支时间谱系中所有语义的逻辑。