An Event Structure Model for Probabilistic Concurrent Kleene Algebra

TL;DR

This paper introduces a novel true-concurrent probabilistic event structure model for probabilistic concurrent Kleene algebra, integrating ideas from existing probabilistic concurrency theories to enhance algebraic reasoning and inference techniques.

Contribution

It presents a new probabilistic event structure model for concurrent Kleene algebra, combining concepts from prior probabilistic concurrency frameworks and analyzing its algebraic properties.

Findings

Model effectively captures true concurrency in probabilistic settings

Enables derivation of probabilistic rely/guarantee inference rules

Provides a basis for algebraic reasoning in probabilistic concurrency

Abstract

We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the model are summarised to the extent that they can be used to derive techniques such as probabilistic rely/guarantee inference rules.