Model Checking Linear Temporal Logic with Standpoint Modalities

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung

Beitragende

Abstract

Standpoint linear temporal logic (SLTL) is a recently introduced extension of 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. Further 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.

Details

OriginalspracheEnglisch
TitelKR 2025 - Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning
Redakteure/-innenMagdalena Ortiz, Renata Wassermann, Torsten Schaub
Herausgeber (Verlag)Association for the Advancement of Artificial Intelligence
Seiten2-11
Seitenumfang10
ISBN (elektronisch)978-1-956792-08-9
PublikationsstatusVeröffentlicht - Nov. 2025
Peer-Review-StatusJa

Publikationsreihe

ReiheProceedings of the International Conference on Knowledge Representation and Reasoning
Band2025-November
ISSN2334-1025

Konferenz

Titel22nd International Conference on Principles of Knowledge Representation and Reasoning
KurztitelKR 2025
Veranstaltungsnummer22
BeschreibungCo-located with CPAIOR 2025, ICAPS 2025 and NMR 2025
Dauer11 - 17 November 2025
Webseite
OrtMelbourne Connect & University of Melbourne
StadtMelbourne
LandAustralien

Externe IDs

ORCID /0000-0002-5321-9343/work/228232890
ORCID /0000-0003-4829-0476/work/228235094
ORCID /0009-0008-4461-0667/work/228236901

Schlagworte

ASJC Scopus Sachgebiete