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$ 与所有其他非等价的模态公式区分开来，其中每个例子是一个有限带根点的克里普克结构。该定义可限制到特定的框架类和模态语言片段：若一个模态片段 $L$ 中每个公式 $\varphi$ 都存在一个针对 $L$ 的有限表征，且该表征由基于 $F$ 中框架的例子组成，则称 $L$ 在框架类 $F$ 上承认有限表征。有限表征对于形式规约的说明、交互式规约和调试具有实用价值，其存在性也是利用成员查询进行精确可学习性的先决条件。我们证明：仅当 $F$ 的模态逻辑是局部表格化时，完整模态语言才能在框架类 $F$ 上承认有限表征。进而研究由某类连接词自由生成的模态片段中哪些承认有限表征。主要结论是：不含真值常量 $\top$ 和 $\bot$ 的正模态语言在所有框架类上承认有限表征。该结果本质上是最优的：当语言扩展真值常量 $\top$ 或 $\bot$，或引入除极有限形式外的任何否定时，有限表征性将失效。