Pith. sign in

REVIEW

Completeness and Incompleteness of Synchronous Kleene Algebra

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1905.08554 v2 pith:4L46C6LQ submitted 2019-05-21 cs.LO

Jana Wagemaker , Marcello Bonsangue , Tobias Kappé , Jurriaan Rot , Alexandra Silva This is my paper · ORCID
classification cs.LO
keywords kleenealgebrasynchronousaxiomslanguagesemanticsalternativeaxiomatisation
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Pith tools