Titelaufnahme

Titel
Rendezvous-multiple broadcast networks / von Johannes Hafner
Verfasser / Verfasserin Hafner, Johannes
Begutachter / BegutachterinZuleger, Florian
ErschienenWien, 2018
Umfangvi, 68 Seiten : Illustrationen
HochschulschriftTechnische Universität Wien, Diplomarbeit, 2018
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (EN)Parameterized Model Checking / Timed Networks
URNurn:nbn:at:at-ubtuw:1-119571 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Rendezvous-multiple broadcast networks [1.28 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

Automatic software verification is concerned with automatically deciding whether a given model of a computer system satisfies a given specification. The Parameterized model checking problem (PMCP) of networks is the special case of deciding whether a given network (usually of identical processes) satisfies its specification regardless of the number of processes in it. We explore the case where the processes are indeed all identical, and communicate via rendezvous and symmetric broadcast. We map the boundary of decidability of the PMCP in such networks. In particular, we show that the PMCP is decidable for finite runs of such networks, whereas for infinite runs the situation is more involved: the PMCP is undecidable already for networks with only two types of broadcast messages (the case of a single symmetric broadcast is already known to be decidable), but becomes decidable if one introduces certain grouping structures limiting the scope of broadcast messages.

Statistik
Das PDF-Dokument wurde 2 mal heruntergeladen.