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

• DOI: 10.48550/arxiv.1403.3286
• Publication Date: 2014-01-01
• Authors: Sadegh Soudjani; Caspar Gevaerts; Alessandro Abate
• Keywords: FAUST; Abstract state machines

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 specified in MATLAB and abstracted as finite-state chain or decision processes. The abstraction procedure runs employs parallel computations fast manipulations based on vector calculus. abstract formally put relationship with the concrete via user-defined maximum threshold approximation error introduced by procedure. allows exporting to well-known probabilistic checkers, such PRISM MRMC. Alternatively, it can handle internally computation PCTL properties (e.g. safety reach-avoid) model, refine outcomes quantified depends given formula. toolbox available at http://sourceforge.net/projects/faust2/