A quantitative study of fork-join processes with non-deterministic choice: application to the statistical exploration of the state-space

We study concurrent programs with non-deterministic choice, loops and a fork-join style of coordination under the lens of combinatorics. As a starting point, we interpret these programs as combinatorial structures. We propose a framework, based on analytic combinatorics, allowing to analyse their quantitative aspects such as the average number of execution path induced by the choice operator, or the proportion of executions of a program with respect to its number of execution prefixes. Building on this theoretical investigation, we develop efficient algorithms aimed at the statistical exploration of their state-space. The first algorithm is a uniform random sampler of bounded executions, providing a good default exploration strategy. The second algorithm is a uniform random sampler of execution prefixes of a given bounded length, offering a more fine-grained generation tool, thus enabling to bias the exploration in a controlled manner. The fundamental characteristics of these algorithms is that they work on the syntax of the programs and do not require the explicit construction of the state-space.