Abstract

Broadcast protocols model parameterised systems in which a finite but arbitrarily large number of identical processes communicate. Communication takes place by means of rendez-vous (two processes exchange a message) or broadcasts (a process sends a message to all the others). Verification of broadcast protocols is difficult, because the desired properties have to be proved for any number of processes.

Emerson and Namjoshi show in a LICS 98 paper that the well-known Karp-Miller procedure (if you don't know it, don't panic: it will be introduced in the talk) can be applied to broadcast protocols, and they use it to verify safety properties. However, they leave open whether the procedure is guaranteed to terminate or not. We show that it may not terminate. Fortunately, we are also able to give an alternative terminating procedure, which proves that the verification problem for safety properties is decidable. Finally, we show that the verification problem for liveness properties is undecidable.

This is joint work with Alain Finkel and Richard Mayr.