Satisfaction Meets Expectations Computing Expected Values of Probabilistic Hybrid Systems with SMT

Martin Fränzle 1 Tino Teige 1 Andreas Eggers 1
1 Carl Von Ossietzky Universität Oldenburg
Abstract : Stochastic satisfiability modulo theories (SSMT), which is an extension of satisfiability modulo theories with randomized quantification, has successfully been used as a symbolic technique for computing reachability probabilities in probabilistic hybrid systems. Motivated by the fact that several industrial applications call for quantitative measures that go beyond mere reachability probabilities, this paper extends SSMT to compute expected values of probabilistic hybrid systems like, e.g., mean-times to failure. Practical applicability of the proposed approach is demonstrated by a case study from networked automation systems.
Keywords : Probabilistic hybrid system Expected value Formal modeling and analysis Stochastic satisfiability modulo theories
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.168-182, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/inria-00525144
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 11:55:27
Dernière modification le : mardi 3 octobre 2017 - 15:00:23

Identifiants

  • HAL Id : inria-00525144, version 1

Collections

Citation

Martin Fränzle, Tino Teige, Andreas Eggers. Satisfaction Meets Expectations Computing Expected Values of Probabilistic Hybrid Systems with SMT. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.168-182, 2010, Lecture Notes in Computer Science. 〈inria-00525144〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

49

Contact


archive-ouverte@inria.fr