arXiv subjects

Safa Zouari

Publications and source records attributed to Safa Zouari.

3 recordsLinked to original sources

arXiv2026

Bisimulations and Modal Logics for Higher Dimensional Automata

Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in van Glabbeek's spectrum, no modal logic has previously characterised it on HDAs. We introduce several new intermediate equivalences that sit strictly between ST- and hhp-bisimilarity. We show how separating similarity and subsumption of paths leads to a clean formulation of these equivalences, and we present a modal logic that characterises hhp-bisimilarity. Natural fragments characterise ST-bisimilarity and the intermediate notions.

cs.LO↗

arXiv2026

Forgetting Event Order in Higher-Dimensional Automata

Higher dimensional automata (HDAs) provide a geometric model of true concurrency, yet their standard formulation encodes an artificial total order on events. This representational artifact causes a fundamental mismatch between the combinatorial structure of HDAs and their observable behavior, leading to logical asymmetries and complicating the application of categorical tools. In this paper, we resolve this tension by developing a semantics for HDAs that is independent of event order, based on interval ipomsets (partially ordered multisets with interfaces) that preserve only precedence and concurrency. We prove that for any HDA, the traditional ST trace of an execution path corresponds precisely to its associated interval ipomset. On the structural side, we show that the presheaf theoretic presentation with an unordered base and the combinatorial presentation of symmetric HDAs are categorically isomorphic. Finally, by characterizing ST and hereditary history preserving (hhp) bisimulation via ipomset isomorphism, we provide a unified, order free foundation for HDA semantics. Our results resolve several critical ambiguities in the literature: they provide the necessary path category structure to canonically apply the Open Maps framework, eliminate representational artifacts in temporal and modal logics, and bridge systematic mismatches between HDAs and other models of concurrency such as Petri nets.

cs.FL↗

arXiv2024

Bisimulations and Logics for Higher-Dimensional Automata

Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects.

cs.LO↗