4
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ With a finite relational model, your above propositional modal logic statement can be algorithmically turned into classic PL derivation such as the common tableaux tree branching method, so in this sense there's a computable procedure. For your example here $A \to \lozenge A$, you can first assume its negation, ie, $A \land \square \lnot A$. But even $w_1$ is accessible to $w_2, w_3$, under Kripke model we cannot branch into any of them because the modality begins with $\square$, so your original statement is not a tautology. But adding symmetry to K, $A \to \square \lozenge A$ is true... $\endgroup$ Commented Oct 7, 2021 at 17:02

2 Answers 2

Reset to default
2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.