Importance Sampling for Stochastic Timed Automata

Cyrille Jegourel, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Sean Sedwards

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

8 Citations (Scopus)
358 Downloads (Pure)

Abstract

We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.
Original languageEnglish
Title of host publicationDependable Software Engineering : Theories, Tools, and Applications
EditorsMartin Fränzle, Deepak Kapur, Naijin Zhan
Number of pages16
PublisherSpringer
Publication date2016
Pages163-178
ISBN (Print)978-3-319-47676-6
ISBN (Electronic)978-3-319-47677-3
DOIs
Publication statusPublished - 2016
EventSymposium on Dependable Software Engineering Theories, Tools and Applications - Beijing, China, Beijing, China
Duration: 9 Nov 201610 Nov 2016
http://lcs.ios.ac.cn/setta/

Conference

ConferenceSymposium on Dependable Software Engineering Theories, Tools and Applications
LocationBeijing, China
Country/TerritoryChina
CityBeijing
Period09/11/201610/11/2016
Internet address
SeriesLecture Notes in Computer Science
Volume9984
ISSN0302-9743

Keywords

  • importance sampling
  • rare events
  • stochastic timed automata
  • verification
  • model checking

Fingerprint

Dive into the research topics of 'Importance Sampling for Stochastic Timed Automata'. Together they form a unique fingerprint.

Cite this