A truly concurrent synchronization product of Markov chains

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