We study the existence of finite characterisations for modal formulas. A finite characterisation of a modal formula $\varphi$ is a finite collection of positive and negative examples that distinguishes $\varphi$ from every other, non-equivalent modal formula, where an example is a finite pointed Kripke structure. This definition can be restricted to specific frame classes and to fragments of the modal language: a modal fragment $L$ admits finite characterisations with respect to a frame class $F$ if every formula $\varphi\in L$ has a finite characterisation with respect to $L$ consting of examples that are based on frames in $F$. Finite characterisations are useful for illustration, interactive specification, and debugging of formal specifications, and their existence is a precondition for exact learnability with membership queries. We show that the full modal language admits finite characterisations with respect to a frame class $F$ only when the modal logic of $F$ is locally tabular. We then study which modal fragments, freely generated by some set of connectives, admit finite characterisations. Our main result is that the positive modal language without the truth-constants $\top$ and $\bot$ admits finite characterisations w.r.t. the class of all frames. This result is essentially optimal: finite characterizability fails when the language is extended with the truth constant $\top$ or $\bot$ or with all but very limited forms of negation.

翻译：我们研究模态公式的有限刻画存在性问题。模态公式 $\varphi$ 的有限刻画是一组有限的正例和反例，能够将 $\varphi$ 与所有其他非等价的模态公式区分开来，其中示例是有限点化克里普克结构。该定义可限定于特定框架类及模态语言片段：若对于任意公式 $\varphi\in L$，存在基于 $F$ 中框架的 $L$ 有限刻画，则称模态片段 $L$ 在框架类 $F$ 上具有有限刻画性质。有限刻画有助于形式规范的说明、交互式规约以及调试，其存在性是精确可学习性（带成员查询）的前提条件。我们证明：仅当 $F$ 的模态逻辑局部可表时，完整模态语言在框架类 $F$ 上具有有限刻画。继而研究由连接词自由生成的模态片段中哪些具有有限刻画性质。主要结论是：不含真值常元 $\top$ 和 $\bot$ 的正模态语言在所有框架类上具有有限刻画。该结果本质上是最优的：当语言扩展了真值常元 $\top$ 或 $\bot$，或引入了除极其受限形式之外的否定时，有限刻画性质将失去。