Kamp Theorem for Pomset Languages of Higher Dimensional Automata
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918239372574720 |
|---|---|
| author | Clement, Emily Erlich, Enzo Ledent, Jérémy |
| author_facet | Clement, Emily Erlich, Enzo Ledent, Jérémy |
| contents | 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, and show that it is equivalent to FO. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_12493 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Kamp Theorem for Pomset Languages of Higher Dimensional Automata Clement, Emily Erlich, Enzo Ledent, Jérémy Formal Languages and Automata Theory 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, and show that it is equivalent to FO. |
| title | Kamp Theorem for Pomset Languages of Higher Dimensional Automata |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2410.12493 |