During the past few years, a number of verification tools have been
developed for real-time systems in the framework of timed automata
(e.g. KRONOS and UPPAAL). One of the major problems in applying these
tools to industrial-size systems is the huge memory-usage for the
exploration of the state-space of a network (or product) of timed
automata, as the model-checkers must keep information on not only the
control structure of the automata but also the clock values specified
by clock constraints.
In this paper, we present a compact data structure for representing
clock constraints. The data structure is based on an ${\cal O}(n^3)$
algorithm which, given a constraint system over real-valued variables
consisting of bounds on differences, constructs an equivalent system
with a {\sl minimal} number of constraints. In addition, we have
developed an on-the-fly reduction technique to minimize the
space-usage. Based on static analysis of the control structure of a
network of timed automata, we are able to compute a set of symbolic
states that cover all the dynamic loops of the network in an
on-the-fly searching algorithm, and thus ensure termination in
reachability analysis.
The two techniques and their combination have been implemented in the
tool UPPAAL. Our experimental results demonstrate that the
techniques result in truly significant space-reductions: for six
examples from the literature, the space saving is between 75\% and
94\%, and in (nearly) all examples time-performance is improved. Also
noteworthy is the observation that the two techniques are completely
orthogonal.