PSPACE-completeness of bimodal transitive weak-density logic

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Balbiani, Philippe, Gasquet, Olivier
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866916852611940352
author Balbiani, Philippe
Gasquet, Olivier
author_facet Balbiani, Philippe
Gasquet, Olivier
contents Windows have been introduce in \cite{BalGasq25} as a tool for designing polynomial algorithms to check satisfiability of a bimodal logic of weak-density. In this paper, after revisiting the ``folklore'' case of bimodal $\K4$ already treated in \cite{Halpern} but which is worth a fresh review, we show that windows allow to polynomially solve the satisfiability problem when adding transitivity to weak-density, by mixing algorithms for bimodal K together with windows-approach. The conclusion is that both satisfiability and validity are PSPACE-complete for these logics.
format Preprint
id arxiv_https___arxiv_org_abs_2507_14949
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle PSPACE-completeness of bimodal transitive weak-density logic
Balbiani, Philippe
Gasquet, Olivier
Logic in Computer Science
03B45, 68Q17
F.4.1; F.4.3
Windows have been introduce in \cite{BalGasq25} as a tool for designing polynomial algorithms to check satisfiability of a bimodal logic of weak-density. In this paper, after revisiting the ``folklore'' case of bimodal $\K4$ already treated in \cite{Halpern} but which is worth a fresh review, we show that windows allow to polynomially solve the satisfiability problem when adding transitivity to weak-density, by mixing algorithms for bimodal K together with windows-approach. The conclusion is that both satisfiability and validity are PSPACE-complete for these logics.
title PSPACE-completeness of bimodal transitive weak-density logic
topic Logic in Computer Science
03B45, 68Q17
F.4.1; F.4.3
url https://arxiv.org/abs/2507.14949