Reachability in networks of register protocols under stochastic schedulers

DOI10.4230/LIPICS.ICALP.2016.106zbMATH Open1388.68195arXiv1602.05928OpenAlexW2280864594MaRDI QIDQ4598247FDOQ4598247

Authors: Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, Daniel Stan 

Publication date: 19 December 2017

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.

Full work available at URL: https://arxiv.org/abs/1602.05928

Recommendations

• Lazy reachability analysis in distributed systems
• Distributed local strategies in broadcast networks
• On Almost-Sure Properties of Probabilistic Discrete Event Systems
• State explosion in almost-sure probabilistic reachability
• Undecidability results for distributed probabilistic systems

zbMATH Keywords

parametrized systemsnetworks of processescut-off propertyalmost-sure reachabilitystochastic scheduler

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (5)

• Title not available (Why is that?)
• Parameterized verification of coverability in infinite state broadcast networks
• Parameterized analysis of reconfigurable broadcast networks
• Liveness in broadcast networks
• Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent

This page was built for publication: Reachability in networks of register protocols under stochastic schedulers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4598247)