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$ 与所有其他非等价的模态公式区分开来，其中实例为有限带标点的Kripke结构。该定义可限制到特定的框架类和模态语言片段：若每一公式 $\varphi\in L$ 均存在基于框架类 $F$ 中框架的有限刻画，则称模态片段 $L$ 在框架类 $F$ 上允许有限刻画。有限刻画在形式规范的图示、交互式规约及调试中具有实用价值，且其存在性是带成员查询的精确可学习性的前提条件。我们证明：仅当 $F$ 的模态逻辑局部可表格化时，完整模态语言在框架类 $F$ 上才允许有限刻画。继而研究由若干联结词自由生成的模态片段中哪些允许有限刻画。主要结论为：不含真值常量 $\top$ 与 $\bot$ 的正模态语言在全体框架类上允许有限刻画。该结果本质上是最优的：当语言扩展真值常量 $\top$ 或 $\bot$，或引入除极有限形式外的否定时，有限刻画性将失效。