Abstract
We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols, a model introduced in [5]. We show that the procedure suggested in [5] for safety properties may not terminate, whereas termination is guaranteed for the procedure of [1] 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 behavior is undecidable.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - Symposium on Logic in Computer Science |
| Publisher | IEEE |
| Pages | 352-359 |
| Number of pages | 8 |
| ISBN (Print) | 0780357701 |
| State | Published - 1999 |
| Event | Proceedings of the 1999 14th Symposium on Logic in Computer Science, LICS'99 - Trento, Italy Duration: 2 Jul 1999 → 5 Jul 1999 |
Conference
| Conference | Proceedings of the 1999 14th Symposium on Logic in Computer Science, LICS'99 |
|---|---|
| City | Trento, Italy |
| Period | 2/07/99 → 5/07/99 |