 |
Overview
This tool combines binary number decision diagrams (bNDD) with the wPDS library of Stefan Schwoon. NDDs are finite automata used for representing sets of integer vectors satisfying some Presburger formula (in fact NDDs are more expressive than Presburger arithmetic). Right
now, the tool supports forward (semi-)reachability analysis for
pushdown systems weighted by bNDDs and should be considered as work in
process.
Future goals are to identify interesting combinations of pushdown systems and NDDs which permit LTL-model checking.
The interested
programmer may make use of this library in other programs.
Downloads
Contact
The library (with the obvious exception of the wpds library) is written by
Holger Austinat and Michael Luttenberger.
In case of questions, bug reports, etc, please mail to ''luttenml ATAT informatik.uni-stuttgart.de''.
Changes
- 08.07.2005: First public release
Publications
Links
- You can find the 7-Zip file archiver here.
- Further projects using or working on NDDs:
|
|
ml) |
© University of Stuttgart |
legal notice