2026-09-18T02:43:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23951 2026-09-05T18:37:12Z ddc:004 open_access

Linear Temporal Logic with Standpoint Modalities (Invited Talk) Baier, Christel Linear Temporal Logic LTL standpoint logics multi-modal logic model checking Standpoint logics have been introduced in recent work by Alvarez et al. as a multi-modal logic to reason about the integrated knowledge of multiple agents that might have different, possibly contradicting views ("standpoints"). The essential new feature are modalities for expressing that a property is conceivable according to the view of an agent. The talk considers the model checking problem for a standpoint extension of classical linear temporal logic (LTL) with five semantics for the standpoint modalities. The semantics differ in the information an agent can extract from the history. Starting with a generic non-elementary model checking algorithm that is applicable to all five semantics, a more detailed complexity analysis leads to improved upper bounds for four of the semantics. In three cases, the model checking problem turns out to be PSPACE-complete, i.e., not harder than the model checking problem for classical LTL, which stands in contrast to the known EXPSPACE-completeness result for the satisfiability problem for standpoint LTL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christel Baier 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.1 urn:nbn:de:0030-drops-239513 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.1 eng https://creativecommons.org/licenses/by/4.0/legalcode