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

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/

This paper is submitted to the 26th International Conference on Computer Aided Verification (CAV 2014)

Cited by in corpus (12)

• Formal Synthesis of Stochastic Systems via Control Barrier Certificates
• Modular Deep Reinforcement Learning with Temporal Logic Specifications
• Strategy Synthesis for Partially-known Switched Stochastic Systems
• Formal Controller Synthesis for Frequency Regulation Utilising Electric Vehicles
• Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems
• SOCKS: A Stochastic Optimal Control and Reachability Toolbox Using Kernel Methods
• Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning
• Benchmarks for cyber-physical systems: A modular model library for building automation systems (Extended version)
• Multi-layered simulation relations for linear stochastic systems
• Recharging Probably Keeps Batteries Alive
• NNSynth: Neural Network Guided Abstraction-Based Controller Synthesis for Stochastic Systems
• Temporal Logic Verification of Stochastic Systems Using Barrier Certificates