Logic and language results for concurrent models

March 17, 2025

Emily Clement (LIPN)

For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. In this talk, I explain my recent works regarding these models and its timed version.

Temporal logics are a powerful tool to specify properties of computational systems.
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 recent work, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp’s theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp’s theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no auto-concurrency.
In previous work, we worked on lifting decidability and undecidability results from Timed Automata to a timed version of HDA, Higher Dimensional Timed Automata.