Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computational Complexity of Standpoint LTL

Stéphane Demri, Przemysław Andrzej Wałęga

TL;DR

This work analyzes the computational properties of standpoint linear temporal logic $\mathsf{SLTL}$ by establishing $\mathsf{EXPSPACE}$-completeness of satisfiability through logarithmic-space reductions with the multi-dimensional modal logic $\mathsf{PTLxS5}$. It also introduces a PSPACE fragment by restricting the interaction of temporal and standpoint operators, showing a worst-case complexity no higher than $\mathsf{LTL}$ and providing an automata-based decision procedure aided by a normalised small-model property for $\mathsf{PSL}$. The results clarify the complexity landscape for combining standpoint logic with temporal reasoning and offer a tractable fragment suitable for practical reasoning. The methods hinge on tight translations, a refined automata construction, and a new model-theoretic property for $\mathsf{PSL}$, with potential implications for decision procedures and future work on implementation.

Abstract

Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of SLTL. First, we establish logarithmic-space reductions between the satisfiability problems for the multi-dimensional modal logic PTLxS5 and SLTL. This leads to the EXPSPACE-completeness of the satisfiability problem in SLTL, which is a surprising result in view of previous investigations. Next, we present a method of restricting SLTL so that the obtained fragment is a strict extension of both the (non-temporal) standpoint logic and linear-time temporal logic LTL, but the satisfiability problem is PSPACE-complete in this fragment. Thus, we show how to combine standpoint logic with LTL so that the worst-case complexity of the obtained combination is not higher than of pure LTL.

Computational Complexity of Standpoint LTL

TL;DR

This work analyzes the computational properties of standpoint linear temporal logic by establishing -completeness of satisfiability through logarithmic-space reductions with the multi-dimensional modal logic . It also introduces a PSPACE fragment by restricting the interaction of temporal and standpoint operators, showing a worst-case complexity no higher than and providing an automata-based decision procedure aided by a normalised small-model property for . The results clarify the complexity landscape for combining standpoint logic with temporal reasoning and offer a tractable fragment suitable for practical reasoning. The methods hinge on tight translations, a refined automata construction, and a new model-theoretic property for , with potential implications for decision procedures and future work on implementation.

Abstract

Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of SLTL. First, we establish logarithmic-space reductions between the satisfiability problems for the multi-dimensional modal logic PTLxS5 and SLTL. This leads to the EXPSPACE-completeness of the satisfiability problem in SLTL, which is a surprising result in view of previous investigations. Next, we present a method of restricting SLTL so that the obtained fragment is a strict extension of both the (non-temporal) standpoint logic and linear-time temporal logic LTL, but the satisfiability problem is PSPACE-complete in this fragment. Thus, we show how to combine standpoint logic with LTL so that the worst-case complexity of the obtained combination is not higher than of pure LTL.
Paper Structure (17 sections, 12 theorems, 19 equations, 1 figure)

This paper contains 17 sections, 12 theorems, 19 equations, 1 figure.

Table of Contents

  1. Logical Preliminaries
  2. Standpoint linear temporal logic $\mathsf{SLTL}\xspace$
  3. Propositional standpoint logic $\mathsf{PSL}\xspace$
  4. Multi-dimensional modal logic $\mathsf{PTLxS5}\xspace$
  5. Satisfiability for $\mathsf{SLTL}\xspace$ is ExpSpace-complete
  6. Translation from $\mathsf{PTLxS5}\xspace$ to $\mathsf{SLTL}\xspace$
  7. Translation from $\mathsf{SLTL}\xspace$ to $\mathsf{PTLxS5}\xspace$
  8. PSpace Fragment of $\mathsf{SLTL}\xspace$
  9. Computationally challenging behaviour of $\mathsf{SLTL}$
  10. Limiting the interplay between connectives
  11. Concluding Remarks
  12. Proof details for Section \ref{['section-expspace-completeness']}
  13. Proof details for \ref{['reducetoSLTL']}
  14. Proof details for \ref{['reducefromSLTL']}
  15. Proof details for Lemma \ref{['avormulad']}
  16. ...and 2 more sections

Key Result

Lemma 1

$\varphi$ is $\mathsf{PTLxS5}\xspace$-satisfiable iff $\mathfrak{t}_1(\varphi)$ is $\mathsf{SLTL}\xspace$-satisfiable.

Figures (1)

  • Figure 1: Construction of $\mathcal{M}$ from $\mathcal{M}_i'$'s with $N=2$, $S^* = S_1 = \{ * \}$, $S_2 = \{ *, \mathtt{s}_2 \}$, $S_3 = \{ *,\mathtt{s}_2, \mathtt{s}_1 \}$, and $\psi_i = \bigwedge_{\psi \in B_i \cap \mathsf{PSL}\xspace} \psi$

Theorems & Definitions (24)

  • Lemma 1
  • proof : Proof sketch
  • Corollary 2
  • Lemma 3
  • proof : Proof sketch
  • Corollary 4
  • Theorem 5
  • Proposition 6
  • proof
  • Lemma 7
  • ...and 14 more