  FAUST$^2$ is a software tool that generates formal abstractions of (possibly
non-deterministic) discrete-time Markov processes (dtMP) defined over
uncountable (continuous) state spaces. A dtMP model is specified in MATLAB and
abstracted as a finite-state Markov chain or Markov decision processes. The
abstraction procedure runs in MATLAB and employs parallel computations and fast
manipulations based on vector calculus. The abstract model is formally put in
relationship with the concrete dtMP via a user-defined maximum threshold on the
approximation error introduced by the abstraction procedure. FAUST$^2$ allows
exporting the abstract model to well-known probabilistic model checkers, such
as PRISM or MRMC. Alternatively, it can handle internally the computation of
PCTL properties (e.g. safety or reach-avoid) over the abstract model, and
refine the outcomes over the concrete dtMP via a quantified error that depends
on the abstraction procedure and the given formula. The toolbox is available at
http://sourceforge.net/projects/faust2/
