FAUST2 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. FAUST2 allows exporting the abstract model to well-known probabilistic model checkers, such as PRISM or MRMC. lternatively, 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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Gleason, Joseph D.; Vinod, Abraham P.; Oishi, Meeko M. K.: Lagrangian approximations for stochastic reachability of a target tube (2021)
  2. Nejati, Ameneh; Soudjani, Sadegh; Zamani, Majid: Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems (2021)
  3. Peruffo, Andrea; Abate, Alessandro: Formal abstraction and synthesis of parametric stochastic processes (2021)
  4. Santoyo, Cesar; Dutreix, Maxence; Coogan, Samuel: A barrier function approach to finite-time stochastic system verification and control (2021)
  5. Lavaei, Abolfazl; Khaled, Mahmoud; Soudjani, Sadegh; Zamani, Majid: AMYTISS: a parallelized tool on automated controller synthesis for large-scale stochastic systems (2020)
  6. Lavaei, Abolfazl; Soudjani, Sadegh; Zamani, Majid: Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach (2020)
  7. Lavaei, Abolfazl; Soudjani, Sadegh; Zamani, Majid: Compositional abstraction-based synthesis for networks of stochastic switched systems (2020)
  8. Le Co├źnt, Adrien; Fribourg, Laurent; Vacher, Jonathan; Wisniewski, Rafael: Probabilistic reachability and control synthesis for stochastic switched systems using the tamed Euler method (2020)
  9. Cauchi, Nathalie; Abate, Alessandro: Poster abstract: StocHy -- automated verification and synthesis of stochastic processes. (2019)
  10. Vinod, Abraham P.; Gleason, Joseph D.; Oishi, Meeko M. K.: SReachTools: a MATLAB stochastic reachability toolbox (2019)
  11. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  12. Esmaeil Zadeh Soudjani, Sadegh; Majumdar, Rupak: Controller synthesis for reward collecting Markov processes in continuous space (2017)
  13. Fischer, Jeffrey M.; Majumdar, Rupak: Programming by composing filters (2017)
  14. Haesaert, Sofie; Zadeh Soudjani, Sadegh Esmaeil; Abate, Alessandro: Verification of general Markov decision processes by approximate similarity relations and policy refinement (2017)