  We introduce new techniques for the parameterized verification of disjunctive
timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate
via location guards that enable a transition only if there is another process
in a given location. This computational model has been considered in the
literature before, example applications are gossiping clock synchronization
protocols or planning problems. We address the minimum-time reachability
problem (Minreach) in DTNs, and show how to efficiently solve it based on a
novel zone graph algorithm. We further show that solving Minreach allows us to
construct a summary TA capturing exactly the possible behaviors of a single TA
within a DTN of arbitrary size. The combination of these two results enables
the parameterized verification of DTNs, while avoiding the construction of an
exponential-size cutoff system required by existing results. Additionally, we
develop sufficient conditions for solving Minreach and parameterized
verification problems even in certain cases where locations that appear in
location guards can have clock invariants, a case that has usually been
excluded in the literature. Our techniques are also implemented, and
experiments show their practicality.
