Official LSV Web Site
Comparison with other tools
Other tools exist for the verification of unbounded counter automata. The following table shows a comparison between FAST and some of these tools. The main advantages of FAST are that FAST:- has a powerful model which allows to express easily most systems,
- uses acceleration and heuristics to compute automatically the reachability set in most practical cases,
- is user-friendly thanks to its GUI (InterFAST).
model acceleration FAST N Presburger
→ → → x = A. x + b yes yes yes yes yes LNDD, MONA LASH Z convex sets
→ → → x = A. x + b yes no yes yes yes NDD R convex sets
→ → → x = A. x + b no - yes yes yes RVA TREX Z
xi ≤ xj + c xi ≤ c xi ≥ c
xi = xj + c xi = c yes yes yes yes yes PDBM R
xi = xj xi = 0 yes yes yes yes no PDBM BRAIN N xi ≤ xj + c
→ → → x = A. x + b no - no yes yes period basis BABYLON N xi ≤ xj + c
→ → → x = A. x + b no - no yes no CST HYTECH R convex sets
→ → → x = A. x + b no - yes yes no convex polyhedra ALV Z Presburger Presburger no - yes yes yes OMEGA, BDD
A comparison of different tools for infinite reachability set computation
