10.4230/LIPICS.ICALP.2016.106
Bouyer, Patricia
Patricia
Bouyer
Markey, Nicolas
Nicolas
Markey
Randour, Mickael
Mickael
Randour
Sangnier, Arnaud
Arnaud
Sangnier
Stan, Daniel
Daniel
Stan
Reachability in Networks of Register Protocols under Stochastic Schedulers
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2016
Networks of Processes
Parametrized Systems
Stochastic Scheduler
Almost-sure Reachability
Cut-Off Property
Chatzigiannakis, Ioannis
Ioannis
Chatzigiannakis
Mitzenmacher, Michael
Michael
Mitzenmacher
Rabani, Yuval
Yuval
Rabani
Sangiorgi, Davide
Davide
Sangiorgi
2016
2016-08-23
2016-08-23
2016-08-23
en
urn:nbn:de:0030-drops-62416
10.4230/LIPIcs.ICALP.2016
978-3-95977-013-2
1868-8969
10.4230/LIPIcs.ICALP.2016
LIPIcs, Volume 55, ICALP 2016
43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
2016
55
106
106:1
106:14
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Chatzigiannakis, Ioannis
Ioannis
Chatzigiannakis
Mitzenmacher, Michael
Michael
Mitzenmacher
Rabani, Yuval
Yuval
Rabani
Sangiorgi, Davide
Davide
Sangiorgi
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2016
55
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
14 pages
571169 bytes
application/pdf
Creative Commons Attribution 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), pages 106:1-106:14