FAUST 2 : Formal Abstractions of Uncountable-STate STochastic Processes

Abstract

FAUST $^{\mathsf 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 a Markov decision process. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vector calculus, which allows scaling beyond state-of-the-art alternatives. 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 $^{\mathsf 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. FAUST $^{\mathsf 2}$ allows refining the outcomes of the verification procedures over the concrete dtMP in view of the quantified and tunable error, which depends on the dtMP dynamics and on the given formula. The toolbox is available at http://sourceforge.net/projects/faust2/