Higher-dimensional automata (HDAs) are models of non-in\-ter\-leav\-ing 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 ST-bisimulation existing in the literature. 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）是非交错并发模型，用于分析并发系统。已有大量文献研究并发系统的互模拟关系，其中部分已扩展至高维自动机。然而，目前尚无针对高维自动机的这些关系的逻辑刻画。本文通过引入Ipomset模态逻辑（一种基于高维自动机的Hennessy-Milner型逻辑）填补了这一空白，并证明该逻辑能够刻画路径互模拟（Path-bisimulation），即文献中ST互模拟的一种变体。我们还利用Joyal、Nielsen和Winskel提出的开放映射框架定义了单元互模拟（Cell-bisimulation）概念，并建立了这些互模拟关系（及其考虑限制条件的"强"变体）之间的联系。在研究中，我们依赖于将高维自动机定义为并发列表上的预层这一新的范畴论定义，以及轨道对象。