FARN WANG2020-06-042020-06-04200303029743https://www.scopus.com/inward/record.uri?eid=2-s2.0-35248884302&doi=10.1007%2f3-540-36384-x_17&partnerID=40&md5=1d8cf1e2c22bfb8d3f45bd49e0b04f1dWe 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. © Springer-Verlag Berlin Heidelberg 2003.BDD; Data-structures; Model-checking; Timed automata; VerificationAutomata theory; Boolean functions; Data structures; Efficiency; State space methods; Verification; BDD; Canonical form; Forward-and-backward; State space representation; Timed Automata; Variable order; Model checkingconference paper10.1007/3-540-36384-X_172-s2.0-35248884302https://doi.org/10.1007/3-540-36384-X_17