Is there a computable procedure for testing whether a given modal schema is true in a given finite relational model?

Question

Is there a computable procedure for testing whether a given modal schema is true in a given finite relational model?

---

This is inspired by question 2 on page 19 by internal numbering (PDF page 34) of the full build of Boxes and Diamonds. (Warning: some spoilers for exercises)

That question is about the truth of the schema $A \to \lozenge A$ in model $M$, where $A$ is an arbitrary formula.

The model $M$ is defined as follows.

There are three worlds $w_1, w_2, w_3$.

There are three primitive propositions $p_1, p_2, p_3$.

The accessibility relation $R$ is $\{(w_1, w_2), (w_1, w_3), (w_2, w_3), (w_3, w_3)\}$.

And the valuation function $V$ is defined by $V(w_i, p_j) = 1$ if and only if $i \le j$, otherwise $V(w_i, p_j) = 0$.

We can demonstrate that $A \to \lozenge A$ doesn't hold everywhere by picking $A$ to be equal to $\lnot p_2$ and picking $w_1$.

$\lnot p_2$ holds at $w_1$. However $\lnot p_2$ fails at both $w_2$ and $w_3$, therefore the original formula $A \to \lozenge A$ is not true.

However, this was a lucky guess and naively testing all possible combinations of formulas and worlds would take infinite time.

This got me wondering: is there a computable procedure for testing whether a given modal schema is true in a finite relational model?

Answer 1

Since normal modal logics are robustly decidable the existence of such procedures should come as no surprise. Indeed, there's much work in modal logic on classes of algorithms that for a given pointed Kripke model $(M, w)$ and a modal formula $\varphi$ decide in a finite number of steps, whether $\varphi$ is true in $(M,w)$ or not given a certain computational bound. Such algorithms are typically called 'model checkers'.

Much of this work centers around temporal logics and is therefore not easily adaptable to the case of the logic $K$. See for instance L. A. Dennis et al: 'Practical Verification of Decision-Making in Agent-Based Autonomous Systems'. CoRR, abs/1310.2431, 2013.

Recently, there has been efforts to provide model checkers specifically for the logic $K$. See for example J.-M. Lagniez et al.: 'On Checking Kripke Models for Modal Logic K'. In: P. Fontaine et al. (eds.): Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, 69-81.

This publication uses a model checking algorithm that is based on a very simple computation procedure termed 'Algorithm 1' (p.71), which is then optimized in various ways to respect certain complexity bounds.

Answer 2

Here's a direct proof of decidability:

Suppose we're given a finite model $M$. By definition, this $M$ consists of a finite set of worlds $W$, an accessibility relation $R$, a finite set of propositional atoms $P$, and a valuation function $v$. Given a modal scheme $\mathscr{S}$, here's how we test whether $\mathscr{S}$ is true in $M$:

The point is that since $M$ is finite, there are only finitely many "definable sets of worlds" - and so only finitely many distinct things we need to plug into $\mathscr{S}$ to test the truth of $\mathscr{S}$ in $M$. Note that it's important we don't overshoot here: not every subset of $W$ is $M$-definable! So even though the full powerset of $W$ is easily computed, we need to be a little cautious about computing the "$M$-definable powerset of $W$" - call it $\mathscr{D}$ - which is the thing we actually care about here.

To compute $\mathscr{D}$, we do the following:

• For $n\in\mathbb{N}$, let $F_n$ be the set of modal formulas in $P$ involving at most $n$ logical symbols (say $\Box,\Diamond,\neg,\wedge,\vee$). Note that each $F_n$ is finite.

• Search for some $n$ such that every subset of $W$ which is $M$-definable by a formula in $F_{2n+1}$ is already $M$-definable by a formula in $F_n$. Since $W$ (and hence $\mathcal{P}(W)$) is finite, we are guaranteed to eventually find such an $n$. Crucially, since the map $\varphi\mapsto\varphi^M$ is computable, this is a step we can actually perform.

• But then it's easy to see that this $F_n$ - or rather, the set of subsets of $W$ defined in $M$ by formulas in this $F_n$ - is all of $\mathscr{D}$. So now we just verify the finitely many occurrences of $\mathscr{S}$ corresponding to formulas in this $F_n$.

Note that this argument is very coarse - it applies, for example, to higher-order modal logics as well.