Model Checking Linear Temporal Logic with Standpoint Modalities

Rajab AghamovRajab Aghamov, Christel BaierChristel Baier, Toghrul KarimovToghrul Karimov, Rupak MajumdarRupak Majumdar, Joël OuaknineJoël Ouaknine, Jakob PiribauerJakob Piribauer, Timm SporkTimm Spork

ISBN: 2334-1033
ISSN: 978-1-956792-08-9

Rajab Aghamov, Christel Baier, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Jakob Piribauer, Timm Spork
Model Checking Linear Temporal Logic with Standpoint Modalities
In Magdalena Ortiz, Renata Wassermann, Torsten Schaub, eds., Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, 2--11, 2025. IJCAI Organization

Details
Bibtex

KurzfassungAbstract
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.
Projekt:Project: CPEC, SECAI
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{KR2025-1,
    title     = [[:Vorlage:Model Checking Linear Temporal Logic with Standpoint Modalities]],
    author    = {Aghamov, Rajab and Baier, Christel and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Joël and Piribauer, Jakob and Spork, Timm},
    booktitle = [[:Vorlage:Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning]],
    pages     = {2--11},
    year      = {2025},
    month     = {10},
    doi       = {10.24963/kr.2025/1},
    url       = {https://doi.org/10.24963/kr.2025/1},
  }