Kamp Theorem for Pomset Languages of Higher Dimensional Automata

TL;DR

This paper extends Kamp's theorem to pomset languages of higher dimensional automata, establishing an equivalence between first-order logic and a newly defined temporal logic for these structures.

Contribution

It introduces a linear temporal logic for pomsets and proves its equivalence to first-order logic, generalizing Kamp's theorem to higher dimensional automata.

Findings

FO-definable pomset languages form a strict subclass of MSO-definable languages

A new LTL for pomsets is equivalent to FO logic

The extension of Kamp's theorem to pomset languages is established

Abstract

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.