Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Complexity of the Constructive Master Modality

Sofía Santiago-Fernández, David Fernández-Duque, Joost J. Joosten

TL;DR

Using translations between logics and fragments of $\sf PDL$, it is shown that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property.

Abstract

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using translations between our logics and fragments of $\sf PDL$, we show that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed $\sf CS4$ and $\sf WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.

The Complexity of the Constructive Master Modality

TL;DR

Using translations between logics and fragments of , it is shown that both and are EXPTIME-complete and admit an exponential-size finite model property.

Abstract

We introduce the semantically-defined constructive master-modality logics and , extending the basic constructive modal logic and the Wijesekera-style logic obtained by impossing infallibility. Using translations between our logics and fragments of , we show that both and are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed and into the master-modality logics, showing that their validity problems are in EXPTIME.
Paper Structure (15 sections, 26 theorems, 5 equations, 3 figures)

This paper contains 15 sections, 26 theorems, 5 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Constructive Master-Modality Logics
  3. Translating $\sf CK^*$ into $\sf WK^*$
  4. Propositional dynamic logic of regular programs
  5. Translating ${\sf WK}^*$ into $\sf PDL$
  6. Upper bounds for the master-modaly logics
  7. Translating $\sf K^*$ into ${\sf CK}^*_\Box$
  8. An application: $\sf CS4$ and $\sf WS4$
  9. Embedding transitive extensions into the Master- Modality logics
  10. Upper bounds for $\sf CS4$ and $\sf WS4$
  11. Concluding remarks
  12. Proof of Proposition \ref{['EqCKWKBox']}
  13. Detailed proofs of the translation from $\sf CK^*$ to $\sf WK^*$
  14. Detailed proofs of the translation from $\sf WK^*$ to $\sf PDL$
  15. Detailed proofs of the translation from $\sf K^*$ to $\sf CK^*$

Key Result

Lemma 2.4

If $\varphi\in\mathcal{L}^*$, $\mathcal{M}$ is any $\sf CK$-model, and $w$ is any world of $\mathcal{M}$, then $(\mathcal{M}, w) \Vdash \Box^* \varphi$ iff for all $v$ such that $w (\preccurlyeq ; R^*)^* v$, $(\mathcal{M},v) \Vdash \varphi$.

Figures (3)

  • Figure 1: Overview of the master-modality logics and the embeddings.
  • Figure 2: Master modalities.
  • Figure 3: Confluence in Lemma \ref{['leqRCS4']}.

Theorems & Definitions (64)

  • Definition 2.1
  • Remark 2.2
  • Remark 2.3: Truth persistence
  • Lemma 2.4
  • proof
  • Definition 2.5
  • Definition 2.6
  • Proposition 2.7
  • Remark 2.8
  • Definition 3.1
  • ...and 54 more