Markov two-components processes

TL;DR

This paper introduces Markov two-components processes (M2CP), a probabilistic model for asynchronous systems that captures partial ordering of time and local independence, extending classical Markov chain concepts to asynchronous settings.

Contribution

It develops the theoretical framework for M2CP, including properties like the Strong Markov property and notions of recurrence, and introduces a synchronization product for Markov chains.

Findings

M2CP are characterized by a finite family of transition matrices.

Local components are conditionally independent given synchronization constraints.

A synchronization product of Markov chains exemplifies M2CP.

Abstract

We propose Markov two-components processes (M2CP) as a probabilistic model of asynchronous systems based on the trace semantics for concurrency. Considering an asynchronous system distributed over two sites, we introduce concepts and tools to manipulate random trajectories in an asynchronous framework: stopping times, an Asynchronous Strong Markov property, recurrent and transient states and irreducible components of asynchronous probabilistic processes. The asynchrony assumption implies that there is no global totally ordered clock ruling the system. Instead, time appears as partially ordered and random. We construct and characterize M2CP through a finite family of transition matrices. M2CP have a local independence property that guarantees that local components are independent in the probabilistic sense, conditionally to their synchronization constraints. A synchronization product of two Markov chains is introduced, as a natural example of M2CP.