Extending BDD technology to dense-time spaces
A model-checker for timed automata.
A simulation/bisimulation checker for timed automata.
A parametric risk analyzer for linear-hybrid automata.
Based on CRD and HRD technology.
¡@
We have moved to Source Forge under the project name of REDLIB.
Please click REDLIB to the Source Forge REDLIB webpage.
** For your interest, RED is also an acronym for Region-Encoding Diagram, the technology used for the first few versions of RED before we changed to CRD.
¡@
Professor Farn Wang
Dept. of Electrical Engineering
National Taiwan University