New data-structure for fully symbolic manipulation of dense-time systems

• Subject: New data-structure for fully symbolic manipulation of dense-time systems
• From: Farn Wang <farn@iis.sinica.edu.tw>
• Date: Fri, 5 Nov 1999 09:15:22 +0800 (CST)
• Cc: farn@iiserv.iis.sinica.edu.tw

Dear fella:

We are happy to announce a new symbolic manipulation technology for
the verification of dense-time systems.  
The technology is called DDD (Data Decision Diagram) for the time being.
DDD is a BDD-like structure for the canonical respresentation of
normalized (explained in the technical report) 
state region sets in a dense-time system.  
Compared to the traditional approach like DBM and CDD, our DDD does
not record the differences between clock readings. 
The innovation of DDD is that we encode the ordering among fractional parts
of clock readings into the variable ordering of DDD.  
For each clock declared, we use one auxiliary binary variable in the DDD 
to record the ordering among sets of the equal fractional parts of clock
readings.  
Thus, unlike DBM technology which requires number of variables quadratic
to the number of clocks, DDD only requires number of variables linear
to the number of clocks.  
Besides, minimal canonicality of DDD follows naturally as in BDD.  

The technical report (TR-IIS-99-009) and experimental tools and data can be
found in webpage 

	http://www.iis.sinica.edu.tw/~farn/ddd

Thanks for reading the message.
Best regards,

	Farn Wang 
	Institute of Information Science
	Academia Sinica
	Taipei, Taiwan 115, ROC
	farn@iis.sinica.edu.tw
	+886-2-27883799 ext. 1717
	FAX:+886-2-27824814

• Prev: International Masters Programme in COMPUTATIONAL LOGIC
• Next: CFP NMR2000 -> abduction
• Index: AMAST Mail - November 1999