2026-07-23T15:19:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6241 2024-03-06T10:37:52Z ddc:004 open_access

Reachability in Networks of Register Protocols under Stochastic Schedulers Bouyer, Patricia Markey, Nicolas Randour, Mickael Sangnier, Arnaud Stan, Daniel Networks of Processes Parametrized Systems Stochastic Scheduler Almost-sure Reachability Cut-Off Property 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Patricia Bouyer and Nicolas Markey and Mickael Randour and Arnaud Sangnier and Daniel Stan 2016 Is Part Of LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2016.106 urn:nbn:de:0030-drops-62416 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.106 eng https://creativecommons.org/licenses/by/3.0/legalcode