| Title: |
Kamp Theorem for Pomset Languages of Higher Dimensional Automata |
| Authors: |
Clement, Emily; Erlich, Enzo; Ledent, Jérémy |
| Contributors: |
Emily Clement and Enzo Erlich and Jérémy Ledent |
| Publisher Information: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Publication Year: |
2026 |
| Collection: |
DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| Subject Terms: |
Higher dimensional automata; temporal logic; Kamp’s theorem |
| Description: |
Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In the case of words, Kamp’s theorem states that First Order (FO) logic is as expressive as Linear Temporal Logic (LTL). In this paper, we extend this result to pomsets. To do so, we first investigate the class of pomset languages that are definable in FO. As expected, this is a strict subclass of MSO-definable languages. Then, we define a Linear Temporal Logic for pomsets (LTL_Poms), and show that it is equivalent to FO. |
| Document Type: |
article in journal/newspaper; conference object |
| File Description: |
application/pdf |
| Language: |
English |
| Relation: |
Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.43 |
| DOI: |
10.4230/LIPIcs.CSL.2026.43 |
| Availability: |
https://doi.org/10.4230/LIPIcs.CSL.2026.43; https://nbn-resolving.org/urn:nbn:de:0030-drops-254685; https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.43 |
| Rights: |
https://creativecommons.org/licenses/by/4.0/legalcode |
| Accession Number: |
edsbas.71F4C126 |
| Database: |
BASE |