TR-IIS-02-009    PDF format

We examine the causes of inefficiencies of previous BDD-like data-structures for timed automata state-space representation and manipulation. We identify four issues, which can cause the inefficiencies: variable designs, normal form definitions, zone-containment relation, and normal form computation. We explore the four issues in details and propose to use CRD (Clock-Restriction Diagram) for timed automata state-space representation. Then instead of using the traditional approach of computing canonical form (i.e., unique normal form) for zones representing the same state-space, we propose the new technique of magnitude derivation and downward redundancy elimination to convert zones into a small range of ˇ§normalizesˇ¨ zones. To better understand the complexity of BDD-like data-structures with various techniques, we have carried out extensive experiments and report the performance of BDD-like data-structures w.r.t. various techniques, benchmarks, and other tools.

keywords: data-structures, BDD, timed automata, verification, model-checking