Presenting Interval Pomsets with Interfaces
Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, Krzysztof Ziemiański
TL;DR
We present an algebraic theory for interval ipomsets by showing they are freely generated by discrete ipomsets (starters and terminators) under gluing, modulo a congruence $\sim$; every interval ipomset (up to isomorphism) corresponds to an equivalence class of step sequences, with a unique sparse representative. Subsumptions are shown to be freely generated by elementary transpositions of starters and terminators, linking the combinatorial and order-theoretic views. On the operational side, we relate higher-dimensional automata (HDAs) to ST-automata via precise translations, proving $L(F(X))=\Phi(L(X))$ while the inverse translation yields language inclusion rather than equality. The paper also identifies open problems, including when a syntactic restriction of ST-automata yields language-preserving translations to HDAs, and discusses interval representations and related literature. Overall, the work unifies a combinatorial and automata-theoretic treatment of interval ipomsets and lays groundwork for algebraic reasoning about concurrency with interfaces, with potential impact on formal models of concurrent computation.
Abstract
Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concurrent systems in which both precedence and concurrency need to be taken into account. In this paper, we develop a presentation of ipomsets as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent terminators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata, which generate ipomsets, and ST-automata, which generate step sequences, and their respective languages.