Region Encoding Diagram for fully symbolic verification of real-time systems

RED (Region Encoding Diagram), first reported by F.Wang (2000), is a BDD-like data structure for fully symbolic verification of symmetric real time systems with single clock per process. We propose to extend RED for asymmetric real time systems with an unrestricted number of global or local clocks. Unlike in DBM which records differences between pairs of clock readings, we record the ordering among fractional parts of clock readings into integer sequences encoded in RED's. Like BDD, the new RED is also a minimal canonical form for its target system state-space representations. The number of variables used in RED is O(|X|log|X|) where X is the clock set in the input system description. Experimentation has been carried out to compare RED's performance with the tools: UPPAAL2K and Kronos. Accordingly, we found out that RED is the most efficient real time system safety analyzer as long as concurrency complexity is considered.