Efficient Verification of Timed Automata using BDDs

Dirk Beyer and Andreas Noack
Software Systems Engineering Research Group
Technical University Cottbus, Germany

Abstract.  This paper investigates the efficient reachability analysis
of timed automata.  It describes a discretization of time which preserves
the reachability properties.  The discretization allows to represent sets
of configurations of timed automata as binary decision diagrams (BDDs).
Further techniques, like computing good variable orderings, are applied
to use the full potential of BDDs as compact and canonical representation
of large sets.  We implemented these concepts within the tool Rabbit.
The highly improved performance is shown for some example models.  For
additional speedup we used an on-the-fly algorithm and refinement
checking for large models.