同步Kleene代数的完备性与不完备性
Completeness and Incompleteness of Synchronous Kleene Algebra
摘要：
同步Kleene代数（SKA）是Kleene代数（KA）的一种扩展，由Prisacariu提出，作为推理可以同步执行的程序的工具，即，步调一致我们提供了一个反模型证明SKA的公理是不完整的w.r.t.它的语言语义，通过利用同步产品操作符和Kleene星之间缺乏交互。然后，我们提出了一套替代的公理SKA，Salomaa的公理化的正则语言的基础上，并表明，这些提供了一个健全的和完整的表征w.r.t.原始语言的语义。
英文摘要：
Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
