Axelerator

Axelerator is a tool for reachability analysis of Open Guarded Linear Time Invariant systems through the use of abstract acceleration. The tool allows the evaluation of reach tubes for both finite and infinite time horizons. System descriptions are in the form of polyhedral sets and discrete dynamics which may be themselves simulations (or bisimulations) of continuous dynamics.

You can download the Linux Source code from the following links:
Original(SAS) version (1.0)
Latest version (1.3)
The package contains both source files and benchmarks to be used as examples. Once the package is extracted, follow the instructions (for Debian/Ubuntu) in Installation.txt.

For a brief decription of how to use the tools, follow the links below:
Usage
File Format

For the paper describing the algorithm follow the links below:
SAS 2015
Extended version

If you have any queries about the tool or the papers, please contact us.