FAUST$^2$: Formal Abstractions of Uncountable-STate STochastic processes

TL;DR

FAUST$^2$ is a MATLAB-based software tool that creates formal finite-state abstractions of uncountable-state stochastic processes, enabling probabilistic model checking with controlled approximation errors.

Contribution

It introduces a novel MATLAB tool for automatically abstracting uncountable-state Markov processes into finite models with error bounds, facilitating formal verification.

Findings

Enables formal abstraction of continuous-state stochastic processes.

Supports probabilistic model checking with error quantification.

Provides efficient parallel computation for abstraction process.

Abstract

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/