Efficient verification of timed automata with BDD-like data structures

We investigate the effect on efficiency of various design issues for BDD-like data structures of TA state space representation and manipulation. We find that the efficiency is highly sensitive to decision atom design and canonical form definition. We explore the two issues in detail and propose to use CRD (Clock-Restriction Diagram) for TA state space representation and present algorithms for manipulating CRD in the verification of TAs. We compare three canonical forms for zones, develop a procedure for quick zone-containment detection, and present algorithms for verification with backward reachability analysis. Three possible evaluation orderings are also considered and discussed. We implement our idea in our tool Red 4.2 and carry out experiments to compare with other tools and various strategies of Red in both forward and backward analysis. Finally, we discuss the possibility of future improvement.