Abstract
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.
Cite
CITATION STYLE
Wagemaker, J., Bonsangue, M., Kappé, T., Rot, J., & Silva, A. (2019). Completeness and Incompleteness of Synchronous Kleene Algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11825 LNCS, pp. 385–413). Springer. https://doi.org/10.1007/978-3-030-33636-3_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
