Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model Checking Linear Temporal Logic with Standpoint Modalities

Rajab Aghamov, Christel Baier, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Jakob Piribauer, Timm Spork

TL;DR

This work extends LTL with standpoint modalities $\langle\langle a \rangle\rangle$ to reason about agents' perspectives over histories, introducing five distinct semantics that govern how much history is visible. It develops a generic model-checking algorithm based on bottom-up construction of history-DFAs for standpoint subformulas and leverages transition-system rewritings and LTL model checking to decide satisfaction. The paper provides tight complexity results: PSPACE-completeness for several cases and $(d-1)$-EXPSPACE or $(N-1)$-EXPSPACE bounds in others, with embeddings into LTLK yielding improved space bounds in many scenarios. Additionally, it shows how SLTL can be embedded into LTLK and into LTLK$_1$ for certain semantics, enabling reductions to known automata-based MC techniques. The results offer a tractable framework for multi-agent reasoning under partial information, with clear avenues for implementing and evaluating the approach on realistic systems.

Abstract

Standpoint linear temporal logic ($SLTL$) is a recently introduced extension of classical linear temporal logic ($LTL$) with standpoint modalities. Intuitively, these modalities allow to express that, from agent $a$'s standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to $SLTL$ under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the $SLTL$ satisfiability problem.

Model Checking Linear Temporal Logic with Standpoint Modalities

TL;DR

This work extends LTL with standpoint modalities to reason about agents' perspectives over histories, introducing five distinct semantics that govern how much history is visible. It develops a generic model-checking algorithm based on bottom-up construction of history-DFAs for standpoint subformulas and leverages transition-system rewritings and LTL model checking to decide satisfaction. The paper provides tight complexity results: PSPACE-completeness for several cases and -EXPSPACE or -EXPSPACE bounds in others, with embeddings into LTLK yielding improved space bounds in many scenarios. Additionally, it shows how SLTL can be embedded into LTLK and into LTLK for certain semantics, enabling reductions to known automata-based MC techniques. The results offer a tractable framework for multi-agent reasoning under partial information, with clear avenues for implementing and evaluating the approach on realistic systems.

Abstract

Standpoint linear temporal logic () is a recently introduced extension of classical linear temporal logic () with standpoint modalities. Intuitively, these modalities allow to express that, from agent 's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the satisfiability problem.

Paper Structure

This paper contains 29 sections, 23 theorems, 6 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. $\mathrm{SLTL}$: LTL with standpoint modalities
  4. Syntax
  5. Semantics of $\mathrm{SLTL}$
  6. From pure observation-based $\mathrm{SLTL}$ to LTLK
  7. Model checking $\mathrm{SLTL}$
  8. Preprocessing for $\models_{ \text{\rm decr}}^{ }$ and $\models_{ \text{\rm incr}}^{ }$.
  9. Observation sets $\mathfrak{O}_{\chi}$.
  10. Transition systems $\mathcal{T}_a^R$.
  11. Basis of induction.
  12. Step of induction.
  13. Final step.
  14. Complexity-theoretic results
  15. Conclusion
  16. ...and 14 more sections

Key Result

Lemma 3.2

If $f_1, f_2\in (2^P)^{\omega}$ and $h \in (2^P)^+$ with $\mathit{last}(h)=\mathit{first}(f_1)=\mathit{first}(f_2)$ then $(f_1,h) \models \langle \!\! \langle a \rangle \!\!\rangle \varphi$ iff $(f_2,h) \models \langle \!\! \langle a \rangle \!\!\rangle \varphi$.

Figures (2)

  • Figure 1: Satisfaction relation $\models$ for $\mathrm{SLTL}$ over future-history pairs $(f,h)\in (2^P)^{\omega}\times (2^P)^+$ with $\mathit{last}(h)=\mathit{first}(f)$.
  • Figure 2: Syntax tree for $\phi = \langle \!\! \langle a \rangle \!\!\rangle p \vee \langle \!\! \langle b \rangle \!\!\rangle (q \wedge \bigcirc \langle \!\! \langle a \rangle \!\!\rangle p)$ and the corresponding satisfaction relations $\models_{ \text{\rm decr}}^{ Q}$ and $\models_{ \text{\rm incr}}^{ Q}$ for the subformulas.

Theorems & Definitions (46)

  • Remark 3.1
  • Lemma 3.2
  • Lemma 3.3
  • Remark 3.4
  • Example 3.5
  • Remark 3.6
  • Lemma 3.7
  • Lemma 3.8
  • Remark 4.1
  • Definition 4.2
  • ...and 36 more