Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 mm1
Verification 6
Subject:
Modelling
Real Time Systems. Timed Automata. UPPAAL.
Time:
23. May 2000
Litterature:
(**) JPK
chapter
4.
(*) Larsen,
Pettersson, Yi: "UPPAAL
in a Nutshell", in Journal for Software Tools for Technology Transfer,
vol 1, 1997.
Model and analyze the following gossiping
girls problem in UPPAAL. A number of girls initially know
one distinct
secret each. Each girl have access to a phone which can be used to call
another girl to
share their secrets.
Each time two girls talk to each other they always exchange all secrets
with each
other (thus after
the phone call they both know all secrets they knew together before the
phone call).
Only binary (between
two girls in each phone call) is possible.
Task 1:
Use UPPAAL to find the minimal number of phone calls needed for four girls
to know all
secrets.
Task 2:
Try to find an (inductive) argument for how many phone calls are needed
to solve the
gossiping girls
problem for n girls.
Task 3: Refine
your model so that each phone call requires start time units to connect,
and in
addition transfer
time units to exchange each secret. Find the minimum time needed to solve
the
gossiping girls
problem for four girls if start is 30 and transfer is 60.