Region Encoding Diagram for Fully Symbolic Verfication of Real-Time Systems
Farn Wang
psfileTR-IIS-00-001
Abstract
RED (Region Encoding Diagram), first reported in TACAS'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 unrestricted number of global
or local clocks. Unlike in DBM which records differences between pairs of clock readings,
we records 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|)$ when $X$ is the clock set in the input
system description.
Experiment has been carried out to show the possible verification efficiency through the intense data-sharing
nature of RED.
¡@
¡@
¡@
¡@
¡@
¡@
¡@