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.

翻译：高阶自动机（HDAs）是用于分析并发系统的非交错并发模型。现有大量文献研究并发系统的互模拟关系，其中部分已扩展至HDAs。然而，目前尚未建立针对HDAs的这些关系的逻辑刻画。本文通过提出Ipomset模态逻辑（一种基于HDAs的Hennessy-Milner类型逻辑）填补了这一空白，并证明该逻辑可刻画路径互模拟——标准ST互模拟的一种变体。我们同时借助Joyal、Nielsen与Winskel的开映射框架定义了单元互模拟概念，并建立了这些互模拟关系（及其考虑限制条件的"强"变体）之间的理论联系。本研究的理论基础依赖于将HDAs重新定义为并发列表上的预层，并引入轨迹对象这一新的范畴论定义。