Title: Rendezvous-multiple broadcast networks
Language: English
Authors: Hafner, Johannes 
Qualification level: Diploma
Advisor: Zuleger, Florian 
Assisting Advisor: Aminof, Benjamin 
Issue Date: 2018
Number of Pages: 68
Qualification level: Diploma
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.
Keywords: Parameterized Model Checking; Timed Networks
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-119571
Library ID: AC15242938
Organisation: E192 - Forschungsbereich Formal Methods in Systems Engineering 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Page view(s)

checked on Jul 7, 2021


checked on Jul 7, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.