oncurrency has an important role in modern systems and programming. It reveals the phenomenon that multiple computations run simultaneously. These interleaved executions cause that the number of states grows exponentially, which is the so-called “state explosion problem”.
In this thesis, we aim at constructing a probabilistic framework on the executions of concurrent systems for the purpose of model checking. Since not all states caused by interleaving are significant, we adopt the partial order semantics, which keeps only one ordering for each set of concurrent actions.
The uniform measure of executions is inspired by trace monoids defined on infinite traces. Trace theory has a strong combinatorial foundation around the Möbius polynomial. The irreducibility of trace monoids implies the strong connectivity of the digraph of cliques. Hence, a dominant eigenvalue exists and determines the growth rate of trace monoids. This completes the probabilistic theory and proves that the finite distributions on trace monoids converge weakly to the uniform measure defined on infinite traces.
However, it is more appropriate to take account of both states and concurrency in realistic systems. In our work, we view the abstract concurrent systems as monoid actions on a finite set of states. This setting encompasses 1-bounded Petri nets. We give two interpretations to a uniform measure of executions for concurrent systems. One is constructed by the elementary cylinders in trace monoids. This uniform measure is realized a Markov chain of states-and-cliques. The other is to study the traces in the finite automaton. In our context, we called it the digraph of states-and-cliques. We want to define the Parry measure on this graph.
The structure of concurrent systems keeps similar combinatorial properties to trace monoids, but it is more complicated. The difficulty to extend to concurrent systems is that the Perron-Frobenius theorem is not applicable. To resolve this problem, we found the spectral property of the irreducible concurrent systems. This allows us to distinguish the main components which determine the characteristic root of the system. We also prove the uniqueness of this uniform measure. The transition matrix can be obtained either from the Markov chain of states-and-cliques with the algorithmic tool or from the Parry measure with the spectral radius of the dominant components. This fulfills the purpose of the random generation.