Advertisement

FAUST\(^{\mathsf 2}\): Formal Abstractions of Uncountable-STate STochastic Processes

  • Sadegh Esmaeil Zadeh SoudjaniEmail author
  • Caspar Gevaerts
  • Alessandro Abate
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

Abstract

FAUST \(^{\mathsf 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 a Markov decision process. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vector 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. FAUST \(^{\mathsf 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. FAUST \(^{\mathsf 2}\) 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. The toolbox is available at http://sourceforge.net/projects/faust2/

Keywords

Markov Decision Process Adaptive Gridding Formal Abstraction Stochastic Kernel Safety Probability 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Meyn, S., Tweedie, R.: Markov chains and stochastic stability. Springer (1993)Google Scholar
  2. 2.
    Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Bertsekas, D., Shreve, S.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (1996)Google Scholar
  4. 4.
    Abate, A., Amin, S., Prandini, M., Lygeros, J., Sastry, S.: Computational approaches to reachability analysis of stochastic hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 4–17. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica 46(12), 1951–1961 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Abate, A., Katoen, J.P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. European Journal of Control 6, 624–641 (2010)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Abate, A., Katoen, J.P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: ACM Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, Chicago, IL, pp. 83–92 (2011)Google Scholar
  8. 8.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive gridding for abstraction and verification of stochastic hybrid systems. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems, pp. 59–69 (September 2011)Google Scholar
  9. 9.
    Tkachev, I., Mereacre, A., Katoen, J., Abate, A.: Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In: Proceedings of the 16th international conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 293–302 (2013)Google Scholar
  10. 10.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems 12(2), 921–956 (2013)Google Scholar
  11. 11.
    Tkachev, I., Abate, A.: Formula-free Finite Abstractions for Linear Temporal Verification of Stochastic Hybrid Systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Philadelphia, PA, pp. 283–292 (April 2013)Google Scholar
  12. 12.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: IEEE Proceedings of the International Conference on Quantitative Evaluation of Systems, Los Alamos, CA, USA, pp. 243–244 (2005)Google Scholar
  14. 14.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  15. 15.
    Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Malhamé, R., Chong, C.: Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system. IEEE Transactions on Automatic Control 30(9), 854–860 (1985)CrossRefzbMATHGoogle Scholar
  17. 17.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Probabilistic invariance of mixed deterministic-stochastic dynamical systems. In: ACM Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control, Beijing, PRC, pp. 207–216 (April 2012)Google Scholar
  18. 18.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Probabilistic reach-avoid computation for partially-degenerate stochastic processes. IEEE Transactions on Automatic Control 59(2), 528–534 (2014)Google Scholar
  19. 19.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Higher-Order Approximations for Verification of Stochastic Hybrid Systems. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 416–434. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Adzkiya, D., Esmaeil Zadeh Soudjani, S., Abate, A.: Finite Abstractions of Stochastic Max-Plus-Linear Systems. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 74–89. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  21. 21.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 547–561. Springer, Heidelberg (2014)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Sadegh Esmaeil Zadeh Soudjani
    • 1
    Email author
  • Caspar Gevaerts
    • 1
  • Alessandro Abate
    • 1
    • 2
  1. 1.Delft Center for Systems and Control (DCSC)TU Delft – Delft University of TechnologyDelftThe Netherlands
  2. 2.Department of Computer ScienceUniversity of OxfordOxfordUK

Personalised recommendations