Reference:

J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proceedings of LICS '99, pages 352–359. IEEE Computer Society, 1999.

Abstract:

We analyse the model-checking problems for safety and liveness properties in parameterised broadcast protocols, a model introduced by Emerson and Namjoshi (LICS '98). We show that the procedure suggested in the paper for safety properties may not terminate, whereas termination is guaranteed for the procedure of Abdulla, Cerans, Jonnson, and Tsay (LICS '96) based on upward closed sets. We show that the model-checking problem for liveness properties is undecidable. In fact, even the problem of deciding if a broadcast protocol may exhibit an infinite behaviour is undecidable.

Suggested BibTeX entry:

@inproceedings{EFM99,
    author = {J. Esparza and A. Finkel and R. Mayr},
    booktitle = {Proceedings of LICS '99},
    pages = {352--359},
    publisher = {IEEE Computer Society},
    title = {On the Verification of Broadcast Protocols},
    year = {1999}
}