We consider families of networks where processes communicate by synchronous broadcast (i.e., a sent message is received by all the neighbours of the emitter) and we study the following safety problem: is there a network in the given family, such that some process can reach an error location? Specifically, we focus on families of network topologies defined by graph grammars, where each node of the produced graph can be either a clique or a cloud (anti-clique) of processes of unbounded sizes. We show that, in general, the considered safety problem is undecidable, when the communication is reliable, and becomes decidable with unreliable communication (i.e., broadcast messages can be lost) or whenever the protocols executed by the different processes cannot send and receive messages from the same control state (also known as the wait-only syntactic restriction).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Safety Analysis in Broadcast Networks Defined by Graph Grammars

  • Christoffer Lind Andersen,
  • Radu Iosif,
  • Arnaud Sangnier

摘要

We consider families of networks where processes communicate by synchronous broadcast (i.e., a sent message is received by all the neighbours of the emitter) and we study the following safety problem: is there a network in the given family, such that some process can reach an error location? Specifically, we focus on families of network topologies defined by graph grammars, where each node of the produced graph can be either a clique or a cloud (anti-clique) of processes of unbounded sizes. We show that, in general, the considered safety problem is undecidable, when the communication is reliable, and becomes decidable with unreliable communication (i.e., broadcast messages can be lost) or whenever the protocols executed by the different processes cannot send and receive messages from the same control state (also known as the wait-only syntactic restriction).