Lookup NU author(s): Dr Sadegh Soudjani
This is the authors' accepted manuscript of a conference proceedings (inc. abstract) that has been published in its final definitive form by Springer, 2015.
For re-use rights please refer to the publisher's terms and conditions.
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 a Markov decision process. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vec- tor 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. FAUST2 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. FAUST2 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.
Author(s): Esmaeil Zadeh Soudjani S, Gevaerts C, Abate A
Editor(s): Baier, C; Tinelli, C
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)
Year of Conference: 2015
Print publication date: 11/04/2015
Acceptance date: 19/12/2014
Date deposited: 08/11/2019
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science