- 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 NPresburger

→ → → x= A.x+ byes yes yes yes yes LNDD, MONA LASH Zconvex sets

→ → → x= A.x+ byes no yes yes yes NDD Rconvex sets

→ → → x= A.x+ bno - yes yes yes RVA TREX Z

x_{i}≤x_{j}+cx_{i}≤cx_{i}≥c

x_{i}=x_{j}+cx_{i}=cyes yes yes yes yes PDBM R

x_{i}=x_{j}x_{i}= 0yes yes yes yes no PDBM BRAIN Nx_{i}≤x_{j}+c

→ → → x= A.x+ bno - no yes yes period basis BABYLON Nx_{i}≤x_{j}+c

→ → → x= A.x+ bno - no yes no CST HYTECH Rconvex sets

→ → → x= A.x+ bno - yes yes no convex polyhedra ALV ZPresburger Presburger no - yes yes yes OMEGA, BDD

A comparison of different tools for infinite reachability set computation