Higher Dimensional Automata Pomset 语言的 Kamp 定理

Emily Clement; Enzo Erlich; Jérémy Ledent

Higher Dimensional Automata Pomset 语言的 Kamp 定理

形式语言与自动机理论 2025-12-10 v4

作者: Emily Clement , Enzo Erlich , Jérémy Ledent

摘要

时序逻辑是指定计算系统属性的强大工具。对于并发程序，Higher Dimensional Automata (HDA) 是一种非常有表现力的非交错并发模型。HDA 识别部分有序多集（pomset）的语言。最近的工作表明，单一次序逻辑（MSO）在 pomset 语言方面的表达力与 HDA 等价。在单词的情况下，Kamp 定理表明，第一阶逻辑（FO）在表达力上等价于线性时序逻辑（LTL）。在本文中，我们将这一结果扩展到 pomset。为此，我们首先研究可在 FO 中定义的 pomset 语言的类别。如预期，这是一个严格的 MSO 可定义语言的子类。然后，我们定义一种用于 pomset 的线性时序逻辑，并证明它等价于 FO。

关键词

时序逻辑 Higher Dimensional Automata pomset Kamp 定理 First Order 逻辑

引用

@article{arxiv.2410.12493,
  title  = {Kamp Theorem for Pomset Languages of Higher Dimensional Automata},
  author = {Emily Clement and Enzo Erlich and Jérémy Ledent},
  journal= {arXiv preprint arXiv:2410.12493},
  year   = {2025}
}

备注

This is the full version of our upcoming CSL 2026 paper. 15 pages + title page + references + appendices

Higher Dimensional Automata Pomset 语言的 Kamp 定理

摘要

关键词

引用

备注

相关论文