Nicolas Markey

Résumé

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.

@inproceedings{icalp2016-BMRSS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Randour,
                         Mickael and Sangnier, Arnaud and Stan, Daniel},
  title =               {Reachability in Networks of Register Protocols under
                         Stochastic Schedulers},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {106:1-106:14},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.106},
  abstract =            {We study the almost-sure reachability problem in a
                         distributed system obtained as the asynchronous
                         composition of~\(N\) copies (called
                         \emph{processes}) of the same automaton (called
                         \emph{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.},
}