Markov two-components processes

We propose Markov two-components processes (M2CP) as a probabilistic model ofasynchronous systems based on the trace semantics for concurrency. Consideringan asynchronous system distributed over two sites, we introduce concepts andtools to manipulate random trajectories in an asynchronous framework: stoppingtimes, an Asynchronous Strong Markov property, recurrent and transient statesand irreducible components of asynchronous probabilistic processes. Theasynchrony assumption implies that there is no global totally ordered clockruling the system. Instead, time appears as partially ordered and random. Weconstruct and characterize M2CP through a finite family of transition matrices.M2CP have a local independence property that guarantees that local componentsare independent in the probabilistic sense, conditionally to theirsynchronization constraints. A synchronization product of two Markov chains isintroduced, as a natural example of M2CP.Comment: 34 page