REDLIB / News: Recent posts

A new version of reference manual has been uploaded that describes how to access the game
synchronous transition tables used in simulation
checking and bisimulation checking.

We have implemented a new version of REDLIB.
The new version supports an integrated software
architecture for the evalaution of time-progress
preconditions with various techniques.

We are glad to announce that now a reference manual for REDLIB in PDF is now available in this sourceforge webpage.
The reference manual explains many of the procedures for basic space manipulations, model-checking, and simulation-checking.
Some procedures implemented for the support of other tools by our collaborators, including a graphical editor, a path explorer, a reachability tree constructor, are not described in the manual. ... read more

As of May 5, 2008, we have made several new releases available. The major change is that we have restored the capabilities of the parametric risk/safety analysis for linear-hybrid automata (LHA).

Together with the new program, you may also find some benchmarks for the parametric analysis of LHA.

Dear ladies/gentlemen:

We are happy to announce REDLIB version 1 after the project was started in 1999 to extend BDD technology for the dense space manipulation. REDLIB is designed to open the capabilities of RED, a model-checker/simulation-checker for timed automata and parametric analyzer for linear hybrid automata, to the publics. At this moment, RED still has the best performance against several benchmarks. In fact, we are still improving its functionalities and performance with new ideas. Now REDLIB supports the following verificaiton tasks. ... read more