Reachability in Networks of Register Protocols under Stochastic Schedulers

Bouyer, Patricia; Markey, Nicolas; Randour, Mickael; Sangnier, Arnaud; Stan, Daniel

doi:10.4230/LIPIcs.ICALP.2016.106

Document

Reachability in Networks of Register Protocols under Stochastic Schedulers

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

Part of: Volume: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Colloquium on Automata, Languages, and Programming (ICALP)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2016-08-23

PDF

File

PDF

LIPIcs.ICALP.2016.106.pdf

Filesize: 0.54 MB
14 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ICALP.2016.106
URN: urn:nbn:de:0030-drops-62416

Subject Classification

Keywords

Networks of Processes
Parametrized Systems
Stochastic Scheduler
Almost-sure Reachability
Cut-Off Property

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 106:1-106:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.106

Author Details

Patricia Bouyer

Nicolas Markey

Mickael Randour

Arnaud Sangnier

Daniel Stan

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail