A truly concurrent synchronization product of Markov chains

In this paper we introduce a product operation on labeled Markov chains. Whereas this kind of product is most usually achieved under an interleaving semantics, for instance in the framework of probabilistic automata, our construction stays within the true-concurrent semantics. Hence the product of two labeled Markov chains we define is a so-called probabilistic Petri net, i.e. a safe Petri net where Mazurkiewicz traces are randomized, not interleavings. We show that this construction is not trivial as far as the number of synchronization transitions is greater or equal than 2. Our main result is that the product of Markov chains remains Markovian, in the sense of probabilistic true-concurrent systems