Satisfiability problems on sums of Kripke frames

TL;DR

This paper investigates the satisfiability problem on sums of Kripke frames, showing under general conditions that it reduces to the satisfiability problem on summands, thus impacting decidability results.

Contribution

It establishes a general condition under which the satisfiability problem on sums of Kripke frames reduces to that of summands, linking decidability properties.

Findings

Satisfiability on sums is polynomial space reducible to summands' satisfiability.

Decidability in PSPACE follows for many modal logics from the semantic characterization.

The paper provides conditions ensuring inheritance of finite model property and decidability.

Abstract

We consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. In many cases, the modal logic of sums inherits the finite model property and decidability from the modal logic of summands. In this paper we show that, under a general condition, the satisfiability problem on sums is polynomial space Turing reducible to the satisfiability problem on summands. In particular, for many modal logics decidability in PSPACE is an immediate corollary from the semantic characterization of the logic.