Model Checking Linear Temporal Logic with Standpoint Modalities
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
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
| Original language | English |
|---|---|
| Title of host publication | KR 2025 - Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning |
| Editors | Magdalena Ortiz, Renata Wassermann, Torsten Schaub |
| Publisher | Association for the Advancement of Artificial Intelligence |
| Pages | 2-11 |
| Number of pages | 10 |
| ISBN (electronic) | 978-1-956792-08-9 |
| Publication status | Published - Nov 2025 |
| Peer-reviewed | Yes |
Publication series
| Series | Proceedings of the International Conference on Knowledge Representation and Reasoning |
|---|---|
| Volume | 2025-November |
| ISSN | 2334-1025 |
Conference
| Title | 22nd International Conference on Principles of Knowledge Representation and Reasoning |
|---|---|
| Abbreviated title | KR 2025 |
| Conference number | 22 |
| Description | Co-located with CPAIOR 2025, ICAPS 2025 and NMR 2025 |
| Duration | 11 - 17 November 2025 |
| Website | |
| Location | Melbourne Connect & University of Melbourne |
| City | Melbourne |
| Country | Australia |
External IDs
| ORCID | /0000-0002-5321-9343/work/228232890 |
|---|---|
| ORCID | /0000-0003-4829-0476/work/228235094 |
| ORCID | /0009-0008-4461-0667/work/228236901 |