10:45  11:45 am, Seminar Hall Parameterized Verification of Coverability in Infinite State Broadcast Networks Balasubramanian A.R. Chennai Mathematical Institute. 290319 Abstract Parameterized verification comprises of studying networks formed of anonymous agents executing the same code which interact with each other through some medium of communication, like broadcast, rendezvous and shared variables. Its aim is to certify the correctness of all instances of the model, independently of the number of agents. Parameterized verification of coverability in broadcast networks with finite state processes has been studied for different types of models and topologies. In this talk, we will introduce a theory of broadcast networks in which the processes can be wellstructured transition systems. The resulting formalism is called wellstructured broadcast networks. For various types of communication topologies, we prove the decidability of coverability in the static case, i.e, when the network topology is not allowed to change. We do this by showing that for these types of static communication topologies, the broadcast network itself is a wellstructured transition system, hence proving the decidability of coverability in the broadcast network. We also give an algorithm to decide coverability of wellstructured broadcast networks when reconfiguration of links between nodes is allowed. Finally, with minor modifications of this algorithm, we prove decidability of coverability when the underlying process is a pushdown automaton.
