Skip to Main content Skip to Navigation
Conference papers

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
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00525144
Contributor : Ist Inria Nancy Grand Est <>
Submitted on : Monday, October 11, 2010 - 11:55:27 AM
Last modification on : Tuesday, October 3, 2017 - 3:00:23 PM

Identifiers

  • 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. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.168-182. ⟨inria-00525144⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

190

 

Contact                    Legal Notice                    Personal Data