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.

翻译：我们研究模态公式的有限刻画存在性问题。模态公式 φ 的有限刻画是由有限个正例和反例构成的集合，该集合能将 φ 与所有其他不等价的模态公式区分开，其中例子是带基点的有限克里普克结构。这一定义可限制到特定的框架类和模态语言片段：若每个公式 φ∈L 均存在基于 F 中框架的有限刻画，则模态片段 L 在框架类 F 上支持有限刻画。有限刻画对于形式规范的图示、交互式规范及调试具有实用价值，其存在性是基于成员查询的精确可学习性的前提条件。我们证明：仅当 F 的模态逻辑局部可表时，完整模态语言才能在框架类 F 上支持有限刻画。进而研究由连接词集自由生成的模态片段中哪些支持有限刻画。主要结论是：不含真值常量 ⊤ 和 ⊥ 的肯定模态语言在所有框架类上支持有限刻画。该结果本质上是最优的：当语言扩展了真值常量 ⊤ 或 ⊥，或引入了除极有限否定形式以外的其他否定时，有限刻画性不再成立。