Recursive windows for grammar logics of bounded density

TL;DR

This paper introduces recursive window techniques for bounded density grammar logics, establishing PSPACE-completeness of their satisfiability and analyzing the monomodal density logic's complexity.

Contribution

It generalizes finite windows to recursive ones in multi-modal logics of bounded density, providing complexity results for satisfiability.

Findings

Satisfiability problem is PSPACE-complete for these logics.

Monomodal density logic is in para-PSPACE.

Recursive windows extend previous finite window approaches.

Abstract

We introduce the family of multi-modal logics of bounded density and with a tableau-like approach using finite \emph{windows} which were introduced in \cite{BalGasq25} and that we generalize to recursive windows. We prove that their satisfiability problem is {\bfseries PSPACE}-complete. As a side effect, the monomodal logic of density is shown to be in para-{\bfseries PSPACE}.