Fully Symbolic Model Checking of Timed Systems using Difference
Decision Diagrams
Jesper Møller
Jakob Lichtenberg
Henrik Reif Andersen
Henrik Hulgaard
July 1999
Abstract
Current approaches for analyzing timed systems are based on an explicit
enumeration of the discrete states and thus these techniques are only
capable of analyzing systems with a handful of timers and a few thousand
states. We address this limitation by describing how to analyze a timed
system fully symbolically, i.e., by representing sets of discrete states and
their associated timing information implicitly. We demonstrate the
efficiency of the symbolic technique by computing the set of reachable
states for a non-trivial timed system and compare the results with the
state-of-the-art tools KRONOS and UPPAAL. With an implementation based on
difference decision diagrams, the runtimes are several orders of magnitudes
better. The key operation in obtaining these results is the ability to
advance time symbolically. We show how to do this efficiently by
essentially quantifying out a special variable z which is used to
represent the constant zero. The symbolic manipulations given in this paper
are sufficient to verify TCTL-formulae fully symbolically.
