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 various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum.

翻译：在刻画模态变迁系统上的模态精化关系的模态逻辑框架中，Boudol和Larsen证明了可将其模型检测归约为预序检测的公式（即特征公式）恰好是那些一致且素性的公式。本文提出了保证特征公式恰好为一致且素性公式的普适充分条件。研究表明，所给条件适用于文献中的多种行为关系。特别地，对于van Glabbeek的线性时间-分支时间谱系中的所有语义，特征公式恰好都是素性且一致的公式。