Characterising Modal Formulas with Examples
Balder ten Cate, Raoul Koudijs
TL;DR
The paper investigates when modal formulas admit finite characterisations, i.e., finite sets of finite pointed Kripke structures that uniquely determine a formula up to logical equivalence. It proves a strong negative result for the full modal language: finite characterisations exist only for frame classes with locally tabular logics; however, a positive, constructive result holds for the positive fragment generated by {Box, Diamond, And, Or} without Top or Bottom, with effective methods to compute such characterisations. The analysis hinges on weak simulations as a semantic foundation, the category of pointed models, and the construction of finite weak-simulation dualities via Fine normal form and a gluing operator, yielding explicit characterisations. The work also establishes size bounds, discusses uniform and poly-modal extensions, and outlines open questions about remaining fragments and restricted frame classes, with implications for illustration, specification debugging, and exact learning with membership queries.
Abstract
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.