Reachability in Networks of Register Protocols under Stochastic Schedulers

TL;DR

This paper investigates the probability of reaching a target state in a distributed system of identical automata with shared registers under stochastic scheduling, revealing a cut-off property and providing an EXPSPACE decision algorithm.

Contribution

It establishes a cut-off property for almost-sure reachability in networks of register protocols and develops an EXPSPACE algorithm to decide the outcome.

Findings

Existence of a cut-off point where the reachability answer stabilizes.

Development of an EXPSPACE algorithm for the decision problem.

Almost-sure reachability depends only on the number of processes once the cut-off is reached.

Abstract

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.