Uniform generation of infinite concurrent runs: the case of trace monoids

TL;DR

This paper presents an algorithm for uniformly generating infinite concurrent runs in systems modeled by trace monoids, enabling on-the-fly approximations that grow linearly over time with distributed computations.

Contribution

It introduces a novel algorithm for uniform generation of infinite runs in concurrent systems modeled by trace monoids, with on-the-fly approximation capabilities.

Findings

Average size of approximation grows linearly with execution time

Algorithm produces distributed computations after precomputations

Outputs approximate infinite runs according to uniform probability measure

Abstract

We introduce an algorithm for the uniform generation of infinite runs in concurrent systems under a partial order probabilistic semantics. We work with trace monoids as concurrency models. The algorithm outputs on-the-fly approximations of a theoretical infinite run, the latter being distributed according to the exact uniform probability measure. The average size of the approximation grows linearly with the time of execution of the algorithm. The execution of the algorithm only involves distributed computations, provided that some - costly - precomputations have been done.