Rendezvous-multiple broadcast networks

Abstract

Automatic software verification is concerned with automatically deciding whether a given model of a computer system satisfies a given specification. The Parameterized model checking problem (PMCP) of networks is the special case of deciding whether a given network (usually of identical processes) satisfies its specification regardless of the number of processes in it. We explore the case where the processes are indeed all identical, and communicate via rendezvous and symmetric broadcast. We map the boundary of decidability of the PMCP in such networks. In particular, we show that the PMCP is decidable for finite runs of such networks, whereas for infinite runs the situation is more involved: the PMCP is undecidable already for networks with only two types of broadcast messages (the case of a single symmetric broadcast is already known to be decidable), but becomes decidable if one introduces certain grouping structures limiting the scope of broadcast messages.