一句话：在共代数上为共归纳谓词建立逻辑完全刻画的一般框架，给出充分条件并实例化相似、发散与行为度量。
经典 Hennessy-Milner 定理表明，像有限的迁移系统中两状态互模拟当且仅当它们满足相同的模态逻辑公式。本文把这一结果从迁移系统推广到共代数，并把互模拟推广为共归纳谓词。作者定义了逻辑对一个共归纳谓词构成完全刻画所需的可靠性与表达性概念，并给出语义层面的充分条件，使得逻辑可用于刻画共归纳谓词。该抽象框架统一处理多种实例：相似性、发散性以及自动机上的行为度量。结果揭示了模态/共代数逻辑与共归纳定义之间的一般联系。
The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.