<div class="csl-bib-body">
<div class="csl-entry">Hafner, J. (2018). <i>Rendezvous-multiple broadcast networks</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.32122</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2018.32122
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/1873
-
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Parameterized Model Checking
en
dc.subject
Timed Networks
en
dc.title
Rendezvous-multiple broadcast networks
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2018.32122
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Johannes Hafner
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Aminof, Benjamin
-
tuw.publication.orgunit
E192 - Forschungsbereich Formal Methods in Systems Engineering