Languages based on the theory of timed automata are a well established
approach for modelling and analysing real-time systems, with many
applications both in industrial and academic context. Model checking
for timed automata has been studied extensively during the last two
decades; however, even now industrial-grade model checkers are
available only for few timed automata dialects (in particular Uppaal
timed automata), exhibit limited scalability for systems with large
discrete state space, or cannot handle parametrised systems. We
explore the use of Horn constraints and off-the-shelf model checkers
for analysis of networks of timed automata.  The resulting analysis
method is fully symbolic and applicable to systems with large or
infinite discrete state space, and can be extended to include various
language features, for instance Uppaal-style communication/broadcast
channels and BIP-style interactions, and systems with infinite
parallelism. Experiments demonstrate the feasibility of the method.