TR-IIS-01-002    zipfile

Farn Wang

¡@Modern model-checkers for real-time systems are usually built around symbolic manipulation pro-cedures of zones, which mean behavior-equivalent dense-time state subspaces and are represented by sets of clock difference constraints. We propose CRD (Clock Restriction Diagram), which is a BDD-like data-structure for recording sets of zones, with related set-oriented operations for fully symbolic verifica- tion of realt-time systems. CRD with zones in reduced from (or reduced CRD in short), which contains minimal number of clock inequalities to characterize a zone, are defined and can be used as a canonical representation for state space. Reduced CRD is more space-efficient than former proposal like DBM, NDD, CDD, and RED. We develop an algorithm that converts given CRDs to reduced CRDs without first computing its closure from(which records the shortest path distance between every pair of clocks) in some representations. We implemented CRD in a new version of our verifier red for timed automata and compare its performance with Kronos's and UPPAAL's against several benchmarks.