同步 Kleene 代数的完备性与不完备性
计算机科学中的逻辑
2023-02-03 v2
摘要
同步 Kleene 代数 (SKA)，是 Kleene 代数 (KA) 的一个扩展，由 Prisacariu 提出，用作推理可能同步执行（即锁步执行）的程序的工具。我们提供了一个反例，证明 SKA 的公理相对于其语言语义不完备，这是通过利用同步积运算子与 Kleene 星之间缺乏相互作用所致。随后，我们提出了基于 Salomaa 对正则语言公理化方案的替代公理集，并证明这些公理相对于原始语言语义提供了完备且 sound 的表征。
引用
@article{arxiv.1905.08554,
title = {Completeness and Incompleteness of Synchronous Kleene Algebra},
author = {Jana Wagemaker and Marcello Bonsangue and Tobias Kappé and Jurriaan Rot and Alexandra Silva},
journal= {arXiv preprint arXiv:1905.08554},
year = {2023}
}
备注
Accepted at MPC 2019