Efficient verification of timed automata with BDD-like data-structures

We investigate the efficiency of BDD-like data-structures for timed automata verification. We find that the efficiency is highly sensitive to the variable designs and canonical form definitions. We explore the two issues in details and propose to use CRD (Clock-Restriction Diagram) for timed automata state-space representation. We compare two canonical forms for zones, develop a procedure for quick zone-containment detection, and discuss the effect of variable-ordering of CRD. We implement our idea in our tool red 4.1 and carry out experiments to compare with other tools and red's previous version in both forward and backward analysis.