  We study the complexity of the model-checking problem for discrete-timed
systems with arbitrarily many anonymous and identical contributors, with and
without a distinguished "controller" process, communicating via synchronous
rendezvous. Our work extends the seminal work on untimed systems by German and
Sistla adding discrete-time clocks, thus allowing one to model more realistic
protocols. For the case without a controller, we show that the systems can be
efficiently simulated -- and vice versa -- by systems of untimed processes
communicating via rendezvous and symmetric broadcast, which we call
"RB-systems". Symmetric broadcast is a novel communication primitive that, like
ordinary asymmetric broadcast, allows all processes to synchronize without
distinction between sender/receiver processes. We show that the complexity of
the parameterized model-checking problem for safety specifications is
pspace-complete, and for liveness specifications it is decidable in exptime.
The latter result required automata theory, rational linear programming, and
geometric reasoning for solving certain reachability questions in a new variant
of vector addition systems called "vector rendezvous systems". We believe such
proof techniques are of independent interest and will be useful in solving
related problems. For the case with a controller, we show that the
parameterized model-checking problems for RB-systems and systems with
asymmetric broadcast are inter-reducible. This implies that for discrete
timed-networks with a controller the parameterized model-checking problem is
undecidable for liveness specifications. Our work exploits the intimate
connection between discrete-timed systems and systems of processes
communicating via broadcast. This allows us to prove decidability results for
liveness properties of parameterized timed-systems, as well as extend work from
untimed systems to timed systems.
