Rare-Event Verification for Stochastic Hybrid Systems

Paolo ZulianiPaolo Zuliani, Christel BaierChristel Baier, Edmund M. ClarkeEdmund M. Clarke

DOI Link

Paolo Zuliani, Christel Baier, Edmund M. Clarke
Rare-Event Verification for Stochastic Hybrid Systems
Proc. of the 15th International Conference on Hybrid Systems: Computation and Control (HSCC'12), 217--226, 2012. ACM Press

Details
Bibtex

KurzfassungAbstract
In this paper we address the problem of verifying in stochastic hybrid systems temporal logic properties whose probability of being true is very small --- rare events. It is well known that sampling-based (Monte Carlo) techniques, such as statistical model checking, do not perform well for estimating rare-event probabilities. The problem is that the sample size required for good accuracy grows too large as the event probability tends to zero. However, several techniques have been developed to address this problem. We focus on importance sampling techniques, which bias the original system to compute highly accurate and efficient estimates. The main difficulty in importance sampling is to devise a good biasing density, that is, a density yielding a low-variance estimator. In this paper, we show how to use the cross-entropy method for generating approximately optimal biasing densities for statistical model checking. We apply the method with importance sampling and statistical model checking for estimating rare-event probabilities in stochastic hybrid systems coded as Stateflow/Simulink diagrams.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{ZBC2012,
  author    = {Paolo Zuliani and Christel Baier and Edmund M. Clarke},
  title     = {Rare-Event Verification for Stochastic Hybrid Systems},
  booktitle = {Proc. of the 15th International Conference on Hybrid Systems:
               Computation and Control (HSCC'12)},
  publisher = {ACM Press},
  year      = {2012},
  pages     = {217--226},
  doi       = {10.1145/2185632.2185665}
}