On the verification of broadcast protocols

Javier Esparza; Alain Finkel; Richard Mayr

On the verification of broadcast protocols

Javier Esparza
, Alain Finkel
, Richard Mayr

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

232 Scopus citations

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

Cite this

@inproceedings{b669aee794ab425ca417811beff0192a,

title = "On the verification of broadcast protocols",

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.",

author = "Javier Esparza and Alain Finkel and Richard Mayr",

year = "1999",

language = "English",

isbn = "0780357701",

pages = "352--359",

booktitle = "Proceedings - Symposium on Logic in Computer Science",

publisher = "IEEE",

note = "Proceedings of the 1999 14th Symposium on Logic in Computer Science, LICS'99 ; Conference date: 02-07-1999 Through 05-07-1999",

}

TY - GEN

T1 - On the verification of broadcast protocols

AU - Esparza, Javier

AU - Finkel, Alain

AU - Mayr, Richard

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/0032597490

M3 - Conference contribution

AN - SCOPUS:0032597490

SN - 0780357701

SP - 352

EP - 359

BT - Proceedings - Symposium on Logic in Computer Science

PB - IEEE

T2 - Proceedings of the 1999 14th Symposium on Logic in Computer Science, LICS'99

Y2 - 2 July 1999 through 5 July 1999

ER -

On the verification of broadcast protocols

Abstract

Conference

Other files and links

Fingerprint

Cite this