Pith. sign in

REVIEW

Partially Observable Concurrent Kleene Algebra

Not yet reviewed by Pith; the record is open.

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 2007.07593 v2 pith:E75NT57A submitted 2020-07-15 cs.LO cs.FLcs.PL

classification cs.LOcs.FLcs.PL
keywords concurrentpockaalgebrakleeneobservablepartiallyprogramsaccess
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

Discussion (0). Continue with ORCID to comment.

Pith tools