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 $\bot$ or with all but very limited forms of negation.

翻译：我们研究模态公式的有限刻画存在性问题。模态公式 $\varphi$ 的有限刻画是一个由正例和反例组成的有限集合，能够将 $\varphi$ 与所有其他非等价的模态公式区分开，其中示例为有限带基点克里普克结构。该定义可限制到特定框架类与模态语言片段：若每个公式 $\varphi\in L$ 均存在基于 $F$ 中框架的 $L$ 有限刻画，则称模态片段 $L$ 关于框架类 $F$ 接纳有限刻画。有限刻画在形式规范的图示、交互式规约及调试中具有重要应用，其存在性是具有成员查询的精确可学习性的先决条件。我们证明：仅当框架类 $F$ 的模态逻辑为局部表格化时，完整模态语言才接纳关于 $F$ 的有限刻画。进而研究由若干连接词自由生成的模态片段中哪些接纳有限刻画。主要结论为：不含真值常元 $\top$ 与 $\bot$ 的正面模态语言关于全框架类接纳有限刻画。该结果本质最优：当语言扩展真值常元 $\bot$ 或几乎所有（极有限形式以外的）否定时，有限刻画性即失效。