Reachability in Networks of Register Protocols under Stochastic Schedulers
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.
Keywords
Cite
@article{arxiv.1602.05928,
title = {Reachability in Networks of Register Protocols under Stochastic Schedulers},
author = {Patricia Bouyer and Nicolas Markey and Mickael Randour and Arnaud Sangnier and Daniel Stan},
journal= {arXiv preprint arXiv:1602.05928},
year = {2016}
}
Comments
Extended version of ICALP 2016 paper