Playing with Probabilities in Reconfigurable Broadcast Networks
Playing with Probabilities in Reconfigurable Broadcast Networks
复制标题
玩转可重构广播网络中的概率
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Arnaud Sangnier
中科院分区：
文献类型：
--
作者：
N. Bertrand;P. Fournier;Arnaud Sangnier
我们研究了具有以下特征的网络模型的验证问题：实体的数量是参数化的，通过广播与相邻邻居进行通信，实体可以概率地改变其内部状态，并且通信拓扑可以随时发生重构。这样一个模型的语义给出了一个无限状态系统的非确定性和概率的选择。我们感兴趣的定性问题，如是否存在一个初始的拓扑结构和决议的非确定性，使配置表现出错误的状态几乎肯定达到。我们表明，所有的定性可达性问题是可判定的，一些证据是基于解决一个2人游戏的可重构网络与广播的奇偶校验和安全目标的图上玩。
We study verification problems for a model of network with the following characteristics: the number of entities is parametric, communication is performed through broadcast with adjacent neighbors, entities can change their internal state probabilistically and reconfiguration of the communication topology can happen at any time. The semantics of such a model is given in term of an infinite state system with both non deterministic and probabilistic choices. We are interested in qualitative problems like whether there exists an initial topology and a resolution of the non determinism such that a configuration exhibiting an error state is almost surely reached. We show that all the qualitative reachability problems are decidable and some proofs are based on solving a 2 player game played on the graphs of a reconfigurable network with broadcast with parity and safety objectives.