一句话：证明高维自动机识别的语言恰为有限区间 pomset 的有理且 subsumption-closed 集合，并建立相应 Kleene 定理。
论文为高维自动机（higher-dimensional automata, HDA）建立了 Kleene 定理，证明其识别的语言恰好是有限区间 pomset 上的有理且 subsumption-closed 集合。为刻画对应的有理运算，作者给 pomset 配备接口，引入一类带接口的高维自动机，并将其建模为带标签 precube 范畴上的 presheaf。证明中发展了受代数拓扑启发的工具与技术，如柱体、纤维化与余纤维化。由于 HDA 是非交错并发的一般模型，可涵盖多种并发方法，而区间序适合事件在时间上延展的并发与分布式系统，因此该工作也可能为其他模型中的 Kleene 定理提供模板。
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
@article{paperbot2700,
title = {Kleene Theorem for Higher-Dimensional Automata},
author = {Uli Fahrenberg and Christian Johansen and Georg Struth and Krzysztof Ziemiański},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:22)2024}
}